# HG changeset patch # User wenzelm # Date 1441828304 -7200 # Node ID 497eb43a306496f857ce10cb0a9571a4c8f3d7a2 # Parent 92858a52e45b7ed4c9c3bce8c06a2bde53fac676# Parent 5e94dfead1c2f370d6120350ad04df3577c610c4 merged diff -r 92858a52e45b -r 497eb43a3064 NEWS --- a/NEWS Wed Sep 09 17:07:51 2015 +0200 +++ b/NEWS Wed Sep 09 21:51:44 2015 +0200 @@ -209,6 +209,10 @@ type_notation Map.map (infixr "~=>" 0) notation Map.map_comp (infixl "o'_m" 55) +* The alternative notation "\" for type and sort constraints has been +removed: in LaTeX document output it looks the same as "::". +INCOMPATIBILITY, use plain "::" instead. + * Case combinator "prod_case" with eta-contracted body functions has explicit "uncurry" notation, to provide a compact notation while getting ride of a special case translation. Slight syntactic @@ -311,6 +315,12 @@ *** ML *** +* Simproc programming interfaces have been simplified: +Simplifier.make_simproc and Simplifier.define_simproc supersede various +forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that +term patterns for the left-hand sides are specified with implicitly +fixed variables, like top-level theorem statements. INCOMPATIBILITY. + * Instantiation rules have been re-organized as follows: Thm.instantiate (*low-level instantiation with named arguments*) diff -r 92858a52e45b -r 497eb43a3064 src/Doc/Codegen/Setup.thy --- a/src/Doc/Codegen/Setup.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Doc/Codegen/Setup.thy Wed Sep 09 21:51:44 2015 +0200 @@ -11,18 +11,13 @@ ML_file "../antiquote_setup.ML" ML_file "../more_antiquote.ML" -setup \ -let - val typ = Simple_Syntax.read_typ; -in - Sign.del_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] -end -\ +no_syntax (output) + "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) + "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) + +syntax (output) + "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) + "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) declare [[default_code_width = 74]] diff -r 92858a52e45b -r 497eb43a3064 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 09 21:51:44 2015 +0200 @@ -839,10 +839,6 @@ input is likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}. - \item Constraints may be either written with two literal colons - ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\"}, - which actually looks exactly the same in some {\LaTeX} styles. - \item Dummy variables (written as underscore) may occur in different roles. diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Decision_Procs/langford.ML Wed Sep 09 21:51:44 2015 +0200 @@ -170,11 +170,8 @@ in val reduce_ex_simproc = - Simplifier.make_simproc - {lhss = [@{cpat "\x. ?P x"}], - name = "reduce_ex_simproc", - proc = K proc, - identifier = []}; + Simplifier.make_simproc @{context} "reduce_ex_simproc" + {lhss = [@{term "\x. P x"}], proc = K proc, identifier = []}; end; diff -r 92858a52e45b -r 497eb43a3064 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/HOL.thy Wed Sep 09 21:51:44 2015 +0200 @@ -1446,25 +1446,29 @@ declaration \ fn _ => Induct.map_simpset (fn ss => ss addsimprocs - [Simplifier.simproc_global @{theory} "swap_induct_false" - ["induct_false \ PROP P \ PROP Q"] - (fn _ => - (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) => - if P <> Q then SOME Drule.swap_prems_eq else NONE - | _ => NONE)), - Simplifier.simproc_global @{theory} "induct_equal_conj_curry" - ["induct_conj P Q \ PROP R"] - (fn _ => - (fn _ $ (_ $ P) $ _ => - let - fun is_conj (@{const induct_conj} $ P $ Q) = - is_conj P andalso is_conj Q - | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true - | is_conj @{const induct_true} = true - | is_conj @{const induct_false} = true - | is_conj _ = false - in if is_conj P then SOME @{thm induct_conj_curry} else NONE end - | _ => NONE))] + [Simplifier.make_simproc @{context} "swap_induct_false" + {lhss = [@{term "induct_false \ PROP P \ PROP Q"}], + proc = fn _ => fn _ => fn ct => + (case Thm.term_of ct of + _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) => + if P <> Q then SOME Drule.swap_prems_eq else NONE + | _ => NONE), + identifier = []}, + Simplifier.make_simproc @{context} "induct_equal_conj_curry" + {lhss = [@{term "induct_conj P Q \ PROP R"}], + proc = fn _ => fn _ => fn ct => + (case Thm.term_of ct of + _ $ (_ $ P) $ _ => + let + fun is_conj (@{const induct_conj} $ P $ Q) = + is_conj P andalso is_conj Q + | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true + | is_conj @{const induct_true} = true + | is_conj @{const induct_false} = true + | is_conj _ = false + in if is_conj P then SOME @{thm induct_conj_curry} else NONE end + | _ => NONE), + identifier = []}] |> Simplifier.set_mksimps (fn ctxt => Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) @@ -1731,8 +1735,14 @@ setup \ Code_Preproc.map_pre (fn ctxt => - ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}] - (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)]) + ctxt addsimprocs + [Simplifier.make_simproc @{context} "equal" + {lhss = [@{term HOL.eq}], + proc = fn _ => fn _ => fn ct => + (case Thm.term_of ct of + Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal} + | _ => NONE), + identifier = []}]) \ diff -r 92858a52e45b -r 497eb43a3064 src/HOL/HOLCF/Tools/cont_proc.ML --- a/src/HOL/HOLCF/Tools/cont_proc.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Wed Sep 09 21:51:44 2015 +0200 @@ -8,7 +8,7 @@ val cont_thms: term -> thm list val all_cont_thms: term -> thm list val cont_tac: Proof.context -> int -> tactic - val cont_proc: theory -> simproc + val cont_proc: simproc val setup: theory -> theory end @@ -119,15 +119,17 @@ end local - fun solve_cont ctxt t = + fun solve_cont ctxt ct = let + val t = Thm.term_of ct val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI} in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end in - fun cont_proc thy = - Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont + val cont_proc = + Simplifier.make_simproc @{context} "cont_proc" + {lhss = [@{term "cont f"}], proc = K solve_cont, identifier = []} end -fun setup thy = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc thy]) thy +val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc]) end diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Imperative_HOL/Overview.thy --- a/src/HOL/Imperative_HOL/Overview.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Imperative_HOL/Overview.thy Wed Sep 09 21:51:44 2015 +0200 @@ -8,18 +8,14 @@ begin (* type constraints with spacing *) -setup {* -let - val typ = Simple_Syntax.read_typ; -in - Sign.del_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] -end -*}(*>*) +no_syntax (output) + "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) + "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) + +syntax (output) + "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) + "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) +(*>*) text {* @{text "Imperative HOL"} is a leightweight framework for reasoning diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Int.thy Wed Sep 09 21:51:44 2015 +0200 @@ -775,9 +775,9 @@ declaration \K Int_Arith.setup\ simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | - "(m::'a::linordered_idom) <= n" | + "(m::'a::linordered_idom) \ n" | "(m::'a::linordered_idom) = n") = - \fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\ + \K Lin_Arith.simproc\ subsection\More Inequality Reasoning\ diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Library/Old_SMT/old_smt_real.ML --- a/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Sep 09 21:51:44 2015 +0200 @@ -114,8 +114,10 @@ "x + y = y + x" by auto} -val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ - "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc +val real_linarith_proc = + Simplifier.make_simproc @{context} "fast_real_arith" + {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \ n"}, @{term "(m::real) = n"}], + proc = K Lin_Arith.simproc, identifier = []} (* setup *) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Library/Old_SMT/old_z3_proof_tools.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Sep 09 21:51:44 2015 +0200 @@ -304,9 +304,9 @@ fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) | dest_binop t = raise TERM ("dest_binop", [t]) - fun prove_antisym_le ctxt t = + fun prove_antisym_le ctxt ct = let - val (le, r, s) = dest_binop t + val (le, r, s) = dest_binop (Thm.term_of ct) val less = Const (@{const_name less}, Term.fastype_of le) val prems = Simplifier.prems_of ctxt in @@ -318,9 +318,9 @@ end handle THM _ => NONE - fun prove_antisym_less ctxt t = + fun prove_antisym_less ctxt ct = let - val (less, r, s) = dest_binop (HOLogic.dest_not t) + val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct)) val le = Const (@{const_name less_eq}, Term.fastype_of less) val prems = Simplifier.prems_of ctxt in @@ -343,12 +343,15 @@ addsimps @{thms z3div_def} addsimps @{thms z3mod_def} addsimprocs [@{simproc numeral_divmod}] addsimprocs [ - Simplifier.simproc_global @{theory} "fast_int_arith" [ - "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc, - Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] - prove_antisym_le, - Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"] - prove_antisym_less]) + Simplifier.make_simproc @{context} "fast_int_arith" + {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \ n"}, @{term "(m::int) = n"}], + proc = K Lin_Arith.simproc, identifier = []}, + Simplifier.make_simproc @{context} "antisym_le" + {lhss = [@{term "(x::'a::order) \ y"}], + proc = K prove_antisym_le, identifier = []}, + Simplifier.make_simproc @{context} "antisym_less" + {lhss = [@{term "\ (x::'a::linorder) < y"}], + proc = K prove_antisym_less, identifier = []}]) structure Simpset = Generic_Data ( diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Library/OptionalSugar.thy Wed Sep 09 21:51:44 2015 +0200 @@ -48,14 +48,13 @@ "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)" (* type constraints with spacing *) +no_syntax (output) + "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) + "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) -no_syntax (xsymbols output) - "_constrain" :: "logic => type => logic" ("_\_" [4, 0] 3) - "_constrain" :: "prop' => type => prop'" ("_\_" [4, 0] 3) - -syntax (xsymbols output) - "_constrain" :: "logic => type => logic" ("_ \ _" [4, 0] 3) - "_constrain" :: "prop' => type => prop'" ("_ \ _" [4, 0] 3) +syntax (output) + "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) + "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) (* sorts as intersections *) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/NSA/HyperDef.thy Wed Sep 09 21:51:44 2015 +0200 @@ -337,7 +337,7 @@ *} simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") = - {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct) *} + {* K Lin_Arith.simproc *} subsection {* Exponentials on the Hyperreals *} diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Nat.thy Wed Sep 09 21:51:44 2015 +0200 @@ -1664,8 +1664,8 @@ setup \Lin_Arith.global_setup\ declaration \K Lin_Arith.setup\ -simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") = - \fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\ +simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \ n" | "(m::nat) = n") = + \K Lin_Arith.simproc\ (* Because of this simproc, the arithmetic solver is really only useful to detect inconsistencies among the premises for subgoals which are *not* themselves (in)equalities, because the latter activate diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 09 21:51:44 2015 +0200 @@ -98,12 +98,15 @@ fun permTs_of (Const (@{const_name Nominal.perm}, T) $ t $ u) = fst (dest_permT T) :: permTs_of u | permTs_of _ = []; -fun perm_simproc' ctxt (Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s)) = +fun perm_simproc' ctxt ct = + (case Thm.term_of ct of + Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s) => let val thy = Proof_Context.theory_of ctxt; val (aT as Type (a, []), S) = dest_permT T; val (bT as Type (b, []), _) = dest_permT U; - in if member (op =) (permTs_of u) aT andalso aT <> bT then + in + if member (op =) (permTs_of u) aT andalso aT <> bT then let val cp = cp_inst_of thy a b; val dj = dj_thm_of thy b a; @@ -115,10 +118,11 @@ end else NONE end - | perm_simproc' _ _ = NONE; + | _ => NONE); val perm_simproc = - Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \ (pi2 \ x)"] perm_simproc'; + Simplifier.make_simproc @{context} "perm_simp" + {lhss = [@{term "pi1 \ (pi2 \ x)"}], proc = K perm_simproc', identifier = []}; fun projections ctxt rule = Project_Rule.projections ctxt rule diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Sep 09 21:51:44 2015 +0200 @@ -40,11 +40,15 @@ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI; fun mk_perm_bool_simproc names = - Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt => - fn Const (@{const_name Nominal.perm}, _) $ _ $ t => - if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) - then SOME perm_bool else NONE - | _ => NONE); + Simplifier.make_simproc @{context} "perm_bool" + {lhss = [@{term "perm pi x"}], + proc = fn _ => fn _ => fn ct => + (case Thm.term_of ct of + Const (@{const_name Nominal.perm}, _) $ _ $ t => + if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) + then SOME perm_bool else NONE + | _ => NONE), + identifier = []}; fun transp ([] :: _) = [] | transp xs = map hd xs :: transp (map tl xs); diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Sep 09 21:51:44 2015 +0200 @@ -44,11 +44,15 @@ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI; fun mk_perm_bool_simproc names = - Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt => - fn Const (@{const_name Nominal.perm}, _) $ _ $ t => - if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) - then SOME perm_bool else NONE - | _ => NONE); + Simplifier.make_simproc @{context} "perm_bool" + {lhss = [@{term "perm pi x"}], + proc = fn _ => fn _ => fn ct => + (case Thm.term_of ct of + Const (@{const_name Nominal.perm}, _) $ _ $ t => + if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) + then SOME perm_bool else NONE + | _ => NONE), + identifier = []}; fun transp ([] :: _) = [] | transp xs = map hd xs :: transp (map tl xs); diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Sep 09 21:51:44 2015 +0200 @@ -3,7 +3,7 @@ Author: Julien Narboux, TU Muenchen Methods for simplifying permutations and for analysing equations -involving permutations. +involving permutations. *) (* @@ -18,8 +18,8 @@ [(a,b)] o pi1 o pi2 = .... - rather it tries to permute pi1 over pi2, which - results in a failure when used with the + rather it tries to permute pi1 over pi2, which + results in a failure when used with the perm_(full)_simp tactics *) @@ -67,7 +67,7 @@ val supp_unit = @{thm "supp_unit"}; val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"}; val cp1_aux = @{thm "cp1_aux"}; -val perm_aux_fold = @{thm "perm_aux_fold"}; +val perm_aux_fold = @{thm "perm_aux_fold"}; val supports_fresh_rule = @{thm "supports_fresh"}; (* needed in the process of fully simplifying permutations *) @@ -76,31 +76,32 @@ val weak_congs = [@{thm "if_weak_cong"}] (* debugging *) -fun DEBUG ctxt (msg,tac) = - CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); -fun NO_DEBUG _ (_,tac) = CHANGED tac; +fun DEBUG ctxt (msg,tac) = + CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); +fun NO_DEBUG _ (_,tac) = CHANGED tac; (* simproc that deals with instances of permutations in front *) (* of applications; just adding this rule to the simplifier *) (* would loop; it also needs careful tuning with the simproc *) (* for functions to avoid further possibilities for looping *) -fun perm_simproc_app' ctxt redex = - let - val thy = Proof_Context.theory_of ctxt; +fun perm_simproc_app' ctxt ct = + let + val thy = Proof_Context.theory_of ctxt + val redex = Thm.term_of ct (* the "application" case is only applicable when the head of f is not a *) (* constant or when (f x) is a permuation with two or more arguments *) - fun applicable_app t = + fun applicable_app t = (case (strip_comb t) of (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2 | (Const _,_) => false | _ => true) in - case redex of + case redex of (* case pi o (f x) == (pi o f) (pi o x) *) (Const(@{const_name Nominal.perm}, Type(@{type_name fun}, - [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => + [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => (if (applicable_app f) then let val name = Long_Name.base_name n @@ -111,12 +112,14 @@ | _ => NONE end -val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app" - ["Nominal.perm pi x"] perm_simproc_app'; +val perm_simproc_app = + Simplifier.make_simproc @{context} "perm_simproc_app" + {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app', identifier = []} (* a simproc that deals with permutation instances in front of functions *) -fun perm_simproc_fun' ctxt redex = - let +fun perm_simproc_fun' ctxt ct = + let + val redex = Thm.term_of ct fun applicable_fun t = (case (strip_comb t) of (Abs _ ,[]) => true @@ -124,20 +127,21 @@ | (Const _, _) => true | _ => false) in - case redex of - (* case pi o f == (%x. pi o (f ((rev pi)o x))) *) - (Const(@{const_name Nominal.perm},_) $ pi $ f) => + case redex of + (* case pi o f == (%x. pi o (f ((rev pi)o x))) *) + (Const(@{const_name Nominal.perm},_) $ pi $ f) => (if applicable_fun f then SOME perm_fun_def else NONE) | _ => NONE end -val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun" - ["Nominal.perm pi x"] perm_simproc_fun'; +val perm_simproc_fun = + Simplifier.make_simproc @{context} "perm_simproc_fun" + {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun', identifier = []} (* function for simplyfying permutations *) (* stac contains the simplifiation tactic that is *) (* applied (see (no_asm) options below *) -fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = +fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = ("general simplification of permutations", fn st => SUBGOAL (fn _ => let val ctxt' = ctxt @@ -150,23 +154,23 @@ end) i st); (* general simplification of permutations and permutation that arose from eqvt-problems *) -fun perm_simp stac ctxt = +fun perm_simp stac ctxt = let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"] - in + in perm_simp_gen stac simps [] ctxt end; -fun eqvt_simp stac ctxt = +fun eqvt_simp stac ctxt = let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"] val eqvts_thms = NominalThmDecls.get_eqvt_thms ctxt; - in + in perm_simp_gen stac simps eqvts_thms ctxt end; (* main simplification tactics for permutations *) fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i)); -fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); +fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac @@ -177,18 +181,18 @@ (* applies the perm_compose rule such that *) (* pi o (pi' o lhs) = rhs *) -(* is transformed to *) +(* is transformed to *) (* (pi o pi') o (pi' o lhs) = rhs *) (* *) (* this rule would loop in the simplifier, so some trick is used with *) (* generating perm_aux'es for the outermost permutation and then un- *) (* folding the definition *) -fun perm_compose_simproc' ctxt redex = - (case redex of +fun perm_compose_simproc' ctxt ct = + (case Thm.term_of ct of (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list}, - [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm}, - Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ + [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm}, + Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ pi2 $ t)) => let val thy = Proof_Context.theory_of ctxt @@ -196,7 +200,7 @@ val uname' = Long_Name.base_name uname in if pi1 <> pi2 then (* only apply the composition rule in this case *) - if T = U then + if T = U then SOME (Thm.instantiate' [SOME (Thm.global_ctyp_of thy (fastype_of t))] [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)] @@ -206,16 +210,18 @@ SOME (Thm.instantiate' [SOME (Thm.global_ctyp_of thy (fastype_of t))] [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)] - (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS + (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS cp1_aux))) else NONE end | _ => NONE); -val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose" - ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; +val perm_compose_simproc = + Simplifier.make_simproc @{context} "perm_compose" + {lhss = [@{term "Nominal.perm pi1 (Nominal.perm pi2 t)"}], + proc = K perm_compose_simproc', identifier = []} -fun perm_compose_tac ctxt i = +fun perm_compose_tac ctxt i = ("analysing permutation compositions on the lhs", fn st => EVERY [resolve_tac ctxt [trans] i, @@ -227,11 +233,11 @@ (* unfolds the definition of permutations *) (* applied to functions such that *) -(* pi o f = rhs *) +(* pi o f = rhs *) (* is transformed to *) (* %x. pi o (f ((rev pi) o x)) = rhs *) fun unfold_perm_fun_def_tac ctxt i = - ("unfolding of permutations on functions", + ("unfolding of permutations on functions", resolve_tac ctxt [perm_fun_def RS meta_eq_to_obj_eq RS trans] i) (* applies the ext-rule such that *) @@ -246,14 +252,14 @@ (* since it contains looping rules the "recursion" - depth is set *) (* to 10 - this seems to be sufficient in most cases *) fun perm_extend_simp_tac_i tactical ctxt = - let fun perm_extend_simp_tac_aux tactical ctxt n = + let fun perm_extend_simp_tac_aux tactical ctxt n = if n=0 then K all_tac - else DETERM o + else DETERM o (FIRST' [fn i => tactical ctxt ("splitting conjunctions on the rhs", resolve_tac ctxt [conjI] i), fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i), fn i => tactical ctxt (perm_compose_tac ctxt i), - fn i => tactical ctxt (apply_cong_tac ctxt i), + fn i => tactical ctxt (apply_cong_tac ctxt i), fn i => tactical ctxt (unfold_perm_fun_def_tac ctxt i), fn i => tactical ctxt (ext_fun_tac ctxt i)] THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1)))) @@ -264,7 +270,7 @@ (* unfolds the support definition and strips off the *) (* intros, then applies eqvt_simp_tac *) fun supports_tac_i tactical ctxt i = - let + let val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod] in EVERY [tactical ctxt ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i), @@ -323,11 +329,11 @@ (* tactic that guesses whether an atom is fresh for an expression *) -(* it first collects all free variables and tries to show that the *) +(* it first collects all free variables and tries to show that the *) (* support of these free variables (op supports) the goal *) (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) fun fresh_guess_tac_i tactical ctxt i st = - let + let val goal = nth (cprems_of st) (i - 1) val fin_supp = Proof_Context.get_thms ctxt "fin_supp" val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm" @@ -335,7 +341,7 @@ val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in case Logic.strip_assums_concl (Thm.term_of goal) of - _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => + _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => let val ps = Logic.strip_params (Thm.term_of goal); val Ts = rev (map snd ps); @@ -353,15 +359,15 @@ infer_instantiate ctxt [(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_fresh_rule'; in - (tactical ctxt ("guessing of the right set that supports the goal", + (tactical ctxt ("guessing of the right set that supports the goal", (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i, asm_full_simp_tac ctxt1 (i+2), - asm_full_simp_tac ctxt2 (i+1), + asm_full_simp_tac ctxt2 (i+1), supports_tac_i tactical ctxt i]))) st end - (* when a term-constructor contains more than one binder, it is useful *) + (* when a term-constructor contains more than one binder, it is useful *) (* in nominal_primrecs to try whether the goal can be solved by an hammer *) - | _ => (tactical ctxt ("if it is not of the form _\_, then try the simplifier", + | _ => (tactical ctxt ("if it is not of the form _\_, then try the simplifier", (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st end handle General.Subscript => Seq.empty; @@ -383,7 +389,7 @@ (* Code opied from the Simplifer for setting up the perm_simp method *) (* behaves nearly identical to the simp-method, for example can handle *) -(* options like (no_asm) etc. *) +(* options like (no_asm) etc. *) val no_asmN = "no_asm"; val no_asm_useN = "no_asm_use"; val no_asm_simpN = "no_asm_simp"; diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Sep 09 21:51:44 2015 +0200 @@ -292,7 +292,7 @@ definition "scalar_product v w = (\ (x, y)\zip v w. x * y)" -definition mv :: "('a \ semiring_0) list list \ 'a list \ 'a list" +definition mv :: "('a :: semiring_0) list list \ 'a list \ 'a list" where [simp]: "mv M v = map (scalar_product v) M" text {* This defines the matrix vector multiplication. To work properly @{term @@ -307,7 +307,7 @@ by (auto simp: sparsify_def set_zip) lemma listsum_sparsify[simp]: - fixes v :: "('a \ semiring_0) list" + fixes v :: "('a :: semiring_0) list" assumes "length w = length v" shows "(\x\sparsify w. (\(i, x). v ! i) x * snd x) = scalar_product v w" (is "(\x\_. ?f x) = _") @@ -317,11 +317,11 @@ *) definition [simp]: "unzip w = (map fst w, map snd w)" -primrec insert :: "('a \ 'b \ linorder) => 'a \ 'a list => 'a list" where +primrec insert :: "('a \ 'b :: linorder) => 'a \ 'a list => 'a list" where "insert f x [] = [x]" | "insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)" -primrec sort :: "('a \ 'b \ linorder) \ 'a list => 'a list" where +primrec sort :: "('a \ 'b :: linorder) \ 'a list => 'a list" where "sort f [] = []" | "sort f (x # xs) = insert f x (sort f xs)" diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Product_Type.thy Wed Sep 09 21:51:44 2015 +0200 @@ -1261,8 +1261,10 @@ setup \ Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs - [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}], - proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}]) + [Simplifier.make_simproc @{context} "set comprehension" + {lhss = [@{term "Collect P"}], + proc = K Set_Comprehension_Pointfree.code_simproc, + identifier = []}]) \ diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Rat.thy Wed Sep 09 21:51:44 2015 +0200 @@ -629,7 +629,7 @@ @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, @{thm of_int_minus}, @{thm of_int_diff}, @{thm of_int_of_nat_eq}] - #> Lin_Arith.add_simprocs Numeral_Simprocs.field_divide_cancel_numeral_factor + #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor] #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) \ diff -r 92858a52e45b -r 497eb43a3064 src/HOL/SPARK/Manual/Reference.thy --- a/src/HOL/SPARK/Manual/Reference.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/SPARK/Manual/Reference.thy Wed Sep 09 21:51:44 2015 +0200 @@ -4,7 +4,7 @@ begin syntax (my_constrain output) - "_constrain" :: "logic => type => logic" ("_ \ _" [4, 0] 3) + "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) (*>*) chapter {* HOL-\SPARK{} Reference *} diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Sep 09 21:51:44 2015 +0200 @@ -353,12 +353,15 @@ mk_solver "distinctFieldSolver" (distinctTree_tac names); fun distinct_simproc names = - Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"] - (fn ctxt => - (fn Const (@{const_name HOL.eq}, _) $ x $ y => + Simplifier.make_simproc @{context} "DistinctTreeProver.distinct_simproc" + {lhss = [@{term "x = y"}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of + Const (@{const_name HOL.eq}, _) $ x $ y => Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) (get_fst_success (neq_x_y ctxt x y) names) - | _ => NONE)); + | _ => NONE), + identifier = []}; end; diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Statespace/state_fun.ML Wed Sep 09 21:51:44 2015 +0200 @@ -51,26 +51,29 @@ in val lazy_conj_simproc = - Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"] - (fn ctxt => fn t => - (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) => - let - val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P); - val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2; - in - if isFalse P' then SOME (conj1_False OF [P_P']) - else - let - val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q); - val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2; - in - if isFalse Q' then SOME (conj2_False OF [Q_Q']) - else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q']) - else if P aconv P' andalso Q aconv Q' then NONE - else SOME (conj_cong OF [P_P', Q_Q']) - end - end - | _ => NONE)); + Simplifier.make_simproc @{context} "lazy_conj_simp" + {lhss = [@{term "P & Q"}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of + Const (@{const_name HOL.conj},_) $ P $ Q => + let + val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P); + val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2; + in + if isFalse P' then SOME (conj1_False OF [P_P']) + else + let + val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q); + val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2; + in + if isFalse Q' then SOME (conj2_False OF [Q_Q']) + else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q']) + else if P aconv P' andalso Q aconv Q' then NONE + else SOME (conj_cong OF [P_P', Q_Q']) + end + end + | _ => NONE), + identifier = []}; fun string_eq_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt @@ -106,13 +109,14 @@ val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false))); val lookup_simproc = - Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"] - (fn ctxt => fn t => - (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ + Simplifier.make_simproc @{context} "lookup_simp" + {lhss = [@{term "lookup d n (update d' c m v s)"}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ (s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) => (let val (_::_::_::_::sT::_) = binder_types uT; - val mi = maxidx_of_term t; + val mi = Term.maxidx_of_term (Thm.term_of ct); fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) = let val (_ :: _ :: _ :: fT :: _ :: _) = binder_types uT; @@ -149,7 +153,8 @@ else SOME thm end handle Option.Option => NONE) - | _ => NONE )); + | _ => NONE), + identifier = []}; local @@ -165,9 +170,10 @@ in val update_simproc = - Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"] - (fn ctxt => fn t => - (case t of + Simplifier.make_simproc @{context} "update_simp" + {lhss = [@{term "update d c n v s"}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _ => let val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT; @@ -242,7 +248,7 @@ val ctxt1 = put_simpset ss' ctxt0; val ctxt2 = put_simpset (#1 (Data.get (Context.Proof ctxt0))) ctxt0; in - (case mk_updterm [] t of + (case mk_updterm [] (Thm.term_of ct) of (trm, trm', vars, _, true) => let val eq1 = @@ -253,7 +259,8 @@ in SOME (Thm.transitive eq1 eq2) end | _ => NONE) end - | _ => NONE)); + | _ => NONE), + identifier = []}; end; @@ -269,10 +276,12 @@ in val ex_lookup_eq_simproc = - Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"] - (fn ctxt => fn t => + Simplifier.make_simproc @{context} "ex_lookup_eq_simproc" + {lhss = [@{term "Ex t"}], + proc = fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; val ex_lookup_ss = #2 (Data.get (Context.Proof ctxt)); val ctxt' = ctxt |> Config.put simp_depth_limit 100 |> put_simpset ex_lookup_ss; @@ -316,7 +325,8 @@ val thm' = if swap then swap_ex_eq OF [thm] else thm in SOME thm' end handle TERM _ => NONE) | _ => NONE) - end handle Option.Option => NONE); + end handle Option.Option => NONE, + identifier = []}; end; diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Statespace/state_space.ML Wed Sep 09 21:51:44 2015 +0200 @@ -211,10 +211,15 @@ val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac; val distinct_simproc = - Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] - (fn ctxt => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) => - Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) (neq_x_y ctxt x y) - | _ => NONE)); + Simplifier.make_simproc @{context} "StateSpace.distinct_simproc" + {lhss = [@{term "x = y"}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of + Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) => + Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) + (neq_x_y ctxt x y) + | _ => NONE), + identifier = []}; fun interprete_parent name dist_thm_name parent_expr thy = let diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Sep 09 21:51:44 2015 +0200 @@ -102,13 +102,13 @@ (case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of NONE => NONE | SOME thm' => - (case try (get_match_inst thy (get_lhs thm')) redex of + (case try (get_match_inst thy (get_lhs thm')) (Thm.term_of redex) of NONE => NONE | SOME inst2 => try (Drule.instantiate_normalize inst2) thm')) end fun ball_bex_range_simproc ctxt redex = - case redex of + (case Thm.term_of redex of (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) => calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 @@ -117,7 +117,7 @@ (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) => calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 - | _ => NONE + | _ => NONE) (* Regularize works as follows: @@ -147,17 +147,19 @@ fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})) +val regularize_simproc = + Simplifier.make_simproc @{context} "regularize" + {lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}], + proc = K ball_bex_range_simproc, + identifier = []}; + fun regularize_tac ctxt = let val thy = Proof_Context.theory_of ctxt - val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} - val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} - val simproc = - Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] ball_bex_range_simproc val simpset = mk_minimal_simpset ctxt addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [simproc] + addsimprocs [regularize_simproc] addSolver equiv_solver addSolver quotient_solver val eq_eqvs = eq_imp_rel_get ctxt in diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/SMT/smt_real.ML --- a/src/HOL/Tools/SMT/smt_real.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_real.ML Wed Sep 09 21:51:44 2015 +0200 @@ -98,8 +98,10 @@ (* Z3 proof replay *) -val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ - "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc +val real_linarith_proc = + Simplifier.make_simproc @{context} "fast_real_arith" + {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \ n"}, @{term "(m::real) = n"}], + proc = K Lin_Arith.simproc, identifier = []} (* setup *) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/SMT/z3_replay_util.ML --- a/src/HOL/Tools/SMT/z3_replay_util.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML Wed Sep 09 21:51:44 2015 +0200 @@ -91,9 +91,9 @@ fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) | dest_binop t = raise TERM ("dest_binop", [t]) - fun prove_antisym_le ctxt t = + fun prove_antisym_le ctxt ct = let - val (le, r, s) = dest_binop t + val (le, r, s) = dest_binop (Thm.term_of ct) val less = Const (@{const_name less}, Term.fastype_of le) val prems = Simplifier.prems_of ctxt in @@ -105,9 +105,9 @@ end handle THM _ => NONE - fun prove_antisym_less ctxt t = + fun prove_antisym_less ctxt ct = let - val (less, r, s) = dest_binop (HOLogic.dest_not t) + val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct)) val le = Const (@{const_name less_eq}, Term.fastype_of less) val prems = Simplifier.prems_of ctxt in @@ -124,11 +124,15 @@ addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def} addsimprocs [@{simproc numeral_divmod}, - Simplifier.simproc_global @{theory} "fast_int_arith" [ - "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc, - Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le, - Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"] - prove_antisym_less]) + Simplifier.make_simproc @{context} "fast_int_arith" + {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \ n"}, @{term "(m::int) = n"}], + proc = K Lin_Arith.simproc, identifier = []}, + Simplifier.make_simproc @{context} "antisym_le" + {lhss = [@{term "(x::'a::order) \ y"}], + proc = K prove_antisym_le, identifier = []}, + Simplifier.make_simproc @{context} "antisym_less" + {lhss = [@{term "\ (x::'a::linorder) < y"}], + proc = K prove_antisym_less, identifier = []}]) structure Simpset = Generic_Data ( diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/groebner.ML Wed Sep 09 21:51:44 2015 +0200 @@ -778,17 +778,20 @@ in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv)) (Thm.instantiate' [] [SOME a, SOME b] idl_sub) end - val poly_eq_simproc = + +val poly_eq_simproc = let - fun proc phi ctxt t = - let val th = poly_eq_conv t - in if Thm.is_reflexive th then NONE else SOME th - end - in make_simproc {lhss = [Thm.lhs_of idl_sub], - name = "poly_eq_simproc", proc = proc, identifier = []} - end; - val poly_eq_ss = - simpset_of (put_simpset HOL_basic_ss @{context} + fun proc ct = + let val th = poly_eq_conv ct + in if Thm.is_reflexive th then NONE else SOME th end + in + Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc" + {lhss = [Thm.term_of (Thm.lhs_of idl_sub)], + proc = fn _ => fn _ => proc, identifier = []} + end; + +val poly_eq_ss = + simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms} addsimprocs [poly_eq_simproc]) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/inductive_set.ML Wed Sep 09 21:51:44 2015 +0200 @@ -38,65 +38,68 @@ val anyt = Free ("t", TFree ("'t", [])); fun strong_ind_simproc tab = - Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn ctxt => fn t => - let - fun close p t f = - let val vs = Term.add_vars t [] - in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs)) - (p (fold (Logic.all o Var) vs t) f) - end; - fun mkop @{const_name HOL.conj} T x = - SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x) - | mkop @{const_name HOL.disj} T x = - SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x) - | mkop _ _ _ = NONE; - fun mk_collect p T t = - let val U = HOLogic.dest_setT T - in HOLogic.Collect_const U $ - HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t - end; - fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member}, - Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) = - mkop s T (m, p, S, mk_collect p T (head_of u)) - | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member}, - Type (_, [_, Type (_, [T, _])]))) $ p $ S)) = - mkop s T (m, p, mk_collect p T (head_of u), S) - | decomp _ = NONE; - val simp = - full_simp_tac - (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1; - fun mk_rew t = (case strip_abs_vars t of - [] => NONE - | xs => (case decomp (strip_abs_body t) of - NONE => NONE - | SOME (bop, (m, p, S, S')) => - SOME (close (Goal.prove ctxt [] []) - (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S')))) - (K (EVERY - [resolve_tac ctxt [eq_reflection] 1, - REPEAT (resolve_tac ctxt @{thms ext} 1), - resolve_tac ctxt [iffI] 1, - EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp, - eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE - EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp, - resolve_tac ctxt [UnI2] 1, simp, - eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp, - resolve_tac ctxt [disjI2] 1, simp]]))) - handle ERROR _ => NONE)) - in - case strip_comb t of - (h as Const (name, _), ts) => (case Symtab.lookup tab name of - SOME _ => - let val rews = map mk_rew ts - in - if forall is_none rews then NONE - else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1) - (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt) - rews ts) (Thm.reflexive (Thm.cterm_of ctxt h))) - end - | NONE => NONE) - | _ => NONE - end); + Simplifier.make_simproc @{context} "strong_ind" + {lhss = [@{term "x::'a::{}"}], + proc = fn _ => fn ctxt => fn ct => + let + fun close p t f = + let val vs = Term.add_vars t [] + in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs)) + (p (fold (Logic.all o Var) vs t) f) + end; + fun mkop @{const_name HOL.conj} T x = + SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x) + | mkop @{const_name HOL.disj} T x = + SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x) + | mkop _ _ _ = NONE; + fun mk_collect p T t = + let val U = HOLogic.dest_setT T + in HOLogic.Collect_const U $ + HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t + end; + fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member}, + Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) = + mkop s T (m, p, S, mk_collect p T (head_of u)) + | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member}, + Type (_, [_, Type (_, [T, _])]))) $ p $ S)) = + mkop s T (m, p, mk_collect p T (head_of u), S) + | decomp _ = NONE; + val simp = + full_simp_tac + (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1; + fun mk_rew t = (case strip_abs_vars t of + [] => NONE + | xs => (case decomp (strip_abs_body t) of + NONE => NONE + | SOME (bop, (m, p, S, S')) => + SOME (close (Goal.prove ctxt [] []) + (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S')))) + (K (EVERY + [resolve_tac ctxt [eq_reflection] 1, + REPEAT (resolve_tac ctxt @{thms ext} 1), + resolve_tac ctxt [iffI] 1, + EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp, + eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE + EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp, + resolve_tac ctxt [UnI2] 1, simp, + eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp, + resolve_tac ctxt [disjI2] 1, simp]]))) + handle ERROR _ => NONE)) + in + (case strip_comb (Thm.term_of ct) of + (h as Const (name, _), ts) => + if Symtab.defined tab name then + let val rews = map mk_rew ts + in + if forall is_none rews then NONE + else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1) + (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt) + rews ts) (Thm.reflexive (Thm.cterm_of ctxt h))) + end + else NONE + | _ => NONE) + end, + identifier = []}; (* only eta contract terms occurring as arguments of functions satisfying p *) fun eta_contract p = @@ -312,9 +315,12 @@ fun to_pred_simproc rules = let val rules' = map mk_meta_eq rules in - Simplifier.simproc_global_i @{theory HOL} "to_pred" [anyt] - (fn ctxt => - lookup_rule (Proof_Context.theory_of ctxt) (Thm.prop_of #> Logic.dest_equals) rules') + Simplifier.make_simproc @{context} "to_pred" + {lhss = [anyt], + proc = fn _ => fn ctxt => fn ct => + lookup_rule (Proof_Context.theory_of ctxt) + (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct), + identifier = []} end; fun to_pred_proc thy rules t = diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/int_arith.ML Wed Sep 09 21:51:44 2015 +0200 @@ -20,33 +20,29 @@ That is, m and n consist only of 1s combined with "+", "-" and "*". *) -val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0}; - -val lhss0 = [@{cpat "0::?'a::ring"}]; - -fun proc0 phi ctxt ct = - let val T = Thm.ctyp_of_cterm ct - in if Thm.typ_of T = @{typ int} then NONE else - SOME (Thm.instantiate' [SOME T] [] zeroth) - end; +val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0}); val zero_to_of_int_zero_simproc = - make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc", - proc = proc0, identifier = []}; - -val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1}; + Simplifier.make_simproc @{context} "zero_to_of_int_zero_simproc" + {lhss = [@{term "0::'a::ring"}], + proc = fn _ => fn ctxt => fn ct => + let val T = Thm.ctyp_of_cterm ct in + if Thm.typ_of T = @{typ int} then NONE + else SOME (Thm.instantiate' [SOME T] [] zeroth) + end, + identifier = []}; -val lhss1 = [@{cpat "1::?'a::ring_1"}]; - -fun proc1 phi ctxt ct = - let val T = Thm.ctyp_of_cterm ct - in if Thm.typ_of T = @{typ int} then NONE else - SOME (Thm.instantiate' [SOME T] [] oneth) - end; +val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1}); val one_to_of_int_one_simproc = - make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc", - proc = proc1, identifier = []}; + Simplifier.make_simproc @{context} "one_to_of_int_one_simproc" + {lhss = [@{term "1::'a::ring_1"}], + proc = fn _ => fn ctxt => fn ct => + let val T = Thm.ctyp_of_cterm ct in + if Thm.typ_of T = @{typ int} then NONE + else SOME (Thm.instantiate' [SOME T] [] oneth) + end, + identifier = []}; fun check (Const (@{const_name Groups.one}, @{typ int})) = false | check (Const (@{const_name Groups.one}, _)) = true @@ -66,18 +62,18 @@ [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}]) addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]); -fun sproc phi ctxt ct = - if check (Thm.term_of ct) then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct) - else NONE; +val zero_one_idom_simproc = + Simplifier.make_simproc @{context} "zero_one_idom_simproc" + {lhss = + [@{term "(x::'a::ring_char_0) = y"}, + @{term "(x::'a::linordered_idom) < y"}, + @{term "(x::'a::linordered_idom) \ y"}], + proc = fn _ => fn ctxt => fn ct => + if check (Thm.term_of ct) + then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct) + else NONE, + identifier = []}; -val lhss' = - [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"}, - @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"}, - @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}] - -val zero_one_idom_simproc = - make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", - proc = sproc, identifier = []} fun number_of ctxt T n = if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral})) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/lin_arith.ML Wed Sep 09 21:51:44 2015 +0200 @@ -9,7 +9,7 @@ val pre_tac: Proof.context -> int -> tactic val simple_tac: Proof.context -> int -> tactic val tac: Proof.context -> int -> tactic - val simproc: Proof.context -> term -> thm option + val simproc: Proof.context -> cterm -> thm option val add_inj_thms: thm list -> Context.generic -> Context.generic val add_lessD: thm -> Context.generic -> Context.generic val add_simps: thm list -> Context.generic -> Context.generic diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Sep 09 21:51:44 2015 +0200 @@ -216,10 +216,10 @@ val bal_add2 = @{thm nat_diff_add_eq2} RS trans ); -fun eq_cancel_numerals ctxt ct = EqCancelNumerals.proc ctxt (Thm.term_of ct) -fun less_cancel_numerals ctxt ct = LessCancelNumerals.proc ctxt (Thm.term_of ct) -fun le_cancel_numerals ctxt ct = LeCancelNumerals.proc ctxt (Thm.term_of ct) -fun diff_cancel_numerals ctxt ct = DiffCancelNumerals.proc ctxt (Thm.term_of ct) +val eq_cancel_numerals = EqCancelNumerals.proc +val less_cancel_numerals = LessCancelNumerals.proc +val le_cancel_numerals = LeCancelNumerals.proc +val diff_cancel_numerals = DiffCancelNumerals.proc (*** Applying CombineNumeralsFun ***) @@ -257,7 +257,7 @@ structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); -fun combine_numerals ctxt ct = CombineNumerals.proc ctxt (Thm.term_of ct) +val combine_numerals = CombineNumerals.proc (*** Applying CancelNumeralFactorFun ***) @@ -311,7 +311,8 @@ ); structure LessCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon +( + open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val cancel = @{thm nat_mult_less_cancel1} RS trans @@ -319,18 +320,19 @@ ); structure LeCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon +( + open CancelNumeralFactorCommon val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT val cancel = @{thm nat_mult_le_cancel1} RS trans val neg_exchanges = true ) -fun eq_cancel_numeral_factor ctxt ct = EqCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun less_cancel_numeral_factor ctxt ct = LessCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun le_cancel_numeral_factor ctxt ct = LeCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun div_cancel_numeral_factor ctxt ct = DivCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun dvd_cancel_numeral_factor ctxt ct = DvdCancelNumeralFactor.proc ctxt (Thm.term_of ct) +val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc +val less_cancel_numeral_factor = LessCancelNumeralFactor.proc +val le_cancel_numeral_factor = LeCancelNumeralFactor.proc +val div_cancel_numeral_factor = DivCancelNumeralFactor.proc +val dvd_cancel_numeral_factor = DvdCancelNumeralFactor.proc (*** Applying ExtractCommonTermFun ***) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Wed Sep 09 21:51:44 2015 +0200 @@ -16,8 +16,6 @@ signature NUMERAL_SIMPROCS = sig - val prep_simproc: theory -> string * string list * (Proof.context -> term -> thm option) - -> simproc val trans_tac: Proof.context -> thm option -> tactic val assoc_fold: Proof.context -> cterm -> thm option val combine_numerals: Proof.context -> cterm -> thm option @@ -37,7 +35,7 @@ val div_cancel_numeral_factor: Proof.context -> cterm -> thm option val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option val field_combine_numerals: Proof.context -> cterm -> thm option - val field_divide_cancel_numeral_factor: simproc list + val field_divide_cancel_numeral_factor: simproc val num_ss: simpset val field_comp_conv: Proof.context -> conv end; @@ -45,9 +43,6 @@ structure Numeral_Simprocs : NUMERAL_SIMPROCS = struct -fun prep_simproc thy (name, pats, proc) = - Simplifier.simproc_global thy name pats proc; - fun trans_tac _ NONE = all_tac | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]); @@ -65,7 +60,7 @@ which is not required for cancellation of common factors in divisions. UPDATE: this reasoning no longer applies (number_ring is gone) *) -fun mk_prod T = +fun mk_prod T = let val one = one_of T fun mk [] = one | mk [t] = t @@ -141,7 +136,7 @@ ordering is not well-founded.*) fun num_ord (i,j) = (case int_ord (abs i, abs j) of - EQUAL => int_ord (Int.sign i, Int.sign j) + EQUAL => int_ord (Int.sign i, Int.sign j) | ord => ord); (*This resembles Term_Ord.term_ord, but it puts binary numerals before other @@ -190,7 +185,7 @@ val field_post_simps = post_simps @ [@{thm divide_zero_left}, @{thm divide_1}] - + (*Simplify inverse Numeral1*) val inverse_1s = [@{thm inverse_numeral_1}]; @@ -202,7 +197,7 @@ @{thms add_neg_numeral_left} @ @{thms mult_numeral_left} @ @{thms arith_simps} @ @{thms rel_simps}; - + (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms during re-arrangement*) val non_add_simps = @@ -288,9 +283,9 @@ val bal_add2 = @{thm le_add_iff2} RS trans ); -fun eq_cancel_numerals ctxt ct = EqCancelNumerals.proc ctxt (Thm.term_of ct) -fun less_cancel_numerals ctxt ct = LessCancelNumerals.proc ctxt (Thm.term_of ct) -fun le_cancel_numerals ctxt ct = LeCancelNumerals.proc ctxt (Thm.term_of ct) +val eq_cancel_numerals = EqCancelNumerals.proc +val less_cancel_numerals = LessCancelNumerals.proc +val le_cancel_numerals = LeCancelNumerals.proc structure CombineNumeralsData = struct @@ -350,9 +345,9 @@ structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); -fun combine_numerals ctxt ct = CombineNumerals.proc ctxt (Thm.term_of ct) +val combine_numerals = CombineNumerals.proc -fun field_combine_numerals ctxt ct = FieldCombineNumerals.proc ctxt (Thm.term_of ct) +val field_combine_numerals = FieldCombineNumerals.proc (** Constant folding for multiplication in semirings **) @@ -433,37 +428,40 @@ ) structure LeCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} +( + open CancelNumeralFactorCommon + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT val cancel = @{thm mult_le_cancel_left} RS trans val neg_exchanges = true ) -fun eq_cancel_numeral_factor ctxt ct = EqCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun less_cancel_numeral_factor ctxt ct = LessCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun le_cancel_numeral_factor ctxt ct = LeCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun div_cancel_numeral_factor ctxt ct = DivCancelNumeralFactor.proc ctxt (Thm.term_of ct) -fun divide_cancel_numeral_factor ctxt ct = DivideCancelNumeralFactor.proc ctxt (Thm.term_of ct) +val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc +val less_cancel_numeral_factor = LessCancelNumeralFactor.proc +val le_cancel_numeral_factor = LeCancelNumeralFactor.proc +val div_cancel_numeral_factor = DivCancelNumeralFactor.proc +val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc val field_divide_cancel_numeral_factor = - [prep_simproc @{theory} - ("field_divide_cancel_numeral_factor", - ["((l::'a::field) * m) / n", - "(l::'a::field) / (m * n)", - "((numeral v)::'a::field) / (numeral w)", - "((numeral v)::'a::field) / (- numeral w)", - "((- numeral v)::'a::field) / (numeral w)", - "((- numeral v)::'a::field) / (- numeral w)"], - DivideCancelNumeralFactor.proc)]; + Simplifier.make_simproc @{context} "field_divide_cancel_numeral_factor" + {lhss = + [@{term "((l::'a::field) * m) / n"}, + @{term "(l::'a::field) / (m * n)"}, + @{term "((numeral v)::'a::field) / (numeral w)"}, + @{term "((numeral v)::'a::field) / (- numeral w)"}, + @{term "((- numeral v)::'a::field) / (numeral w)"}, + @{term "((- numeral v)::'a::field) / (- numeral w)"}], + proc = K DivideCancelNumeralFactor.proc, + identifier = []} val field_cancel_numeral_factors = - prep_simproc @{theory} - ("field_eq_cancel_numeral_factor", - ["(l::'a::field) * m = n", - "(l::'a::field) = m * n"], - EqCancelNumeralFactor.proc) - :: field_divide_cancel_numeral_factor; + [Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor" + {lhss = + [@{term "(l::'a::field) * m = n"}, + @{term "(l::'a::field) = m * n"}], + proc = K EqCancelNumeralFactor.proc, + identifier = []}, + field_divide_cancel_numeral_factor] (** Declarations for ExtractCommonTerm **) @@ -476,7 +474,7 @@ handle TERM _ => find_first_t (t::past) u terms; (** Final simplification for the CancelFactor simprocs **) -val simplify_one = Arith_Data.simplify_meta_eq +val simplify_one = Arith_Data.simplify_meta_eq [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; fun cancel_simplify_meta_eq ctxt cancel_th th = @@ -484,7 +482,7 @@ local val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop) - fun Eq_True_elim Eq = + fun Eq_True_elim Eq = Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} in fun sign_conv pos_th neg_th ctxt t = @@ -515,7 +513,7 @@ simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute}) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) - val simplify_meta_eq = cancel_simplify_meta_eq + val simplify_meta_eq = cancel_simplify_meta_eq fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) end; @@ -585,25 +583,26 @@ fun divide_cancel_factor ctxt ct = DivideCancelFactor.proc ctxt (Thm.term_of ct) local - val zr = @{cpat "0"} - val zT = Thm.ctyp_of_cterm zr - val geq = @{cpat HOL.eq} - val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} - val add_frac_num = mk_meta_eq @{thm "add_frac_num"} - val add_num_frac = mk_meta_eq @{thm "add_num_frac"} + +val zr = @{cpat "0"} +val zT = Thm.ctyp_of_cterm zr +val geq = @{cpat HOL.eq} +val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd +val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} +val add_frac_num = mk_meta_eq @{thm "add_frac_num"} +val add_num_frac = mk_meta_eq @{thm "add_num_frac"} - fun prove_nz ctxt T t = - let - val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr - val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq - val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) - (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"} - (Thm.apply (Thm.apply eq t) z))) - in Thm.equal_elim (Thm.symmetric th) TrueI - end +fun prove_nz ctxt T t = + let + val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr + val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq + val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) + (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"} + (Thm.apply (Thm.apply eq t) z))) + in Thm.equal_elim (Thm.symmetric th) TrueI + end - fun proc phi ctxt ct = +fun proc ctxt ct = let val ((x,y),(w,z)) = (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct @@ -611,11 +610,10 @@ val T = Thm.ctyp_of_cterm x val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z] val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq - in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) - end + in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - fun proc2 phi ctxt ct = +fun proc2 ctxt ct = let val (l,r) = Thm.dest_binop ct val T = Thm.ctyp_of_cterm l @@ -636,12 +634,12 @@ end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b - | is_number t = can HOLogic.dest_number t +fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b + | is_number t = can HOLogic.dest_number t - val is_number = is_number o Thm.term_of +val is_number = is_number o Thm.term_of - fun proc3 phi ctxt ct = +fun proc3 ctxt ct = (case Thm.term_of ct of Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => let @@ -685,41 +683,42 @@ val T = Thm.ctyp_of_cterm c val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} in SOME (mk_meta_eq th) end - | _ => NONE) - handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE + | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE val add_frac_frac_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], - name = "add_frac_frac_simproc", - proc = proc, identifier = []} + Simplifier.make_simproc @{context} "add_frac_frac_simproc" + {lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}], + proc = K proc, identifier = []} val add_frac_num_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], - name = "add_frac_num_simproc", - proc = proc2, identifier = []} + Simplifier.make_simproc @{context} "add_frac_num_simproc" + {lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}], + proc = K proc2, identifier = []} val ord_frac_simproc = - make_simproc - {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, - @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, - @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, - @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], - name = "ord_frac_simproc", proc = proc3, identifier = []} + Simplifier.make_simproc @{context} "ord_frac_simproc" + {lhss = + [@{term "(a::'a::{field,ord}) / b < c"}, + @{term "(a::'a::{field,ord}) / b \ c"}, + @{term "c < (a::'a::{field,ord}) / b"}, + @{term "c \ (a::'a::{field,ord}) / b"}, + @{term "c = (a::'a::{field,ord}) / b"}, + @{term "(a::'a::{field, ord}) / b = c"}], + proc = K proc3, identifier = []} -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, - @{thm "divide_numeral_1"}, - @{thm "divide_zero"}, @{thm divide_zero_left}, - @{thm "divide_divide_eq_left"}, - @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, - @{thm "times_divide_times_eq"}, - @{thm "divide_divide_eq_right"}, - @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"}, - @{thm "add_divide_distrib"} RS sym, - @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, - Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute})))) - (@{thm Fields.field_divide_inverse} RS sym)] +val ths = + [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, + @{thm "divide_numeral_1"}, + @{thm "divide_zero"}, @{thm divide_zero_left}, + @{thm "divide_divide_eq_left"}, + @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, + @{thm "times_divide_times_eq"}, + @{thm "divide_divide_eq_right"}, + @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"}, + @{thm "add_divide_distrib"} RS sym, + @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, + Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute})))) + (@{thm Fields.field_divide_inverse} RS sym)] val field_comp_ss = simpset_of @@ -740,4 +739,3 @@ end end; - diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Tools/record.ML Wed Sep 09 21:51:44 2015 +0200 @@ -1059,9 +1059,13 @@ subrecord. *) val simproc = - Simplifier.simproc_global @{theory HOL} "record" ["x"] - (fn ctxt => fn t => - let val thy = Proof_Context.theory_of ctxt in + Simplifier.make_simproc @{context} "record" + {lhss = [@{term "x"}], + proc = fn _ => fn ctxt => fn ct => + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + in (case t of (sel as Const (s, Type (_, [_, rangeS]))) $ ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => @@ -1109,7 +1113,8 @@ end else NONE | _ => NONE) - end); + end, + identifier = []}; fun get_upd_acc_cong_thm upd acc thy ss = let @@ -1139,10 +1144,12 @@ we omit considering further updates if doing so would introduce both a more update and an update to a field within it.*) val upd_simproc = - Simplifier.simproc_global @{theory HOL} "record_upd" ["x"] - (fn ctxt => fn t => + Simplifier.make_simproc @{context} "record_upd" + {lhss = [@{term "x"}], + proc = fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; (*We can use more-updators with other updators as long as none of the other updators go deeper than any more updator. min here is the depth of the deepest other @@ -1240,7 +1247,8 @@ (prove_unfold_defs thy noops' [simproc] (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) else NONE - end); + end, + identifier = []}; end; @@ -1260,16 +1268,19 @@ Complexity: #components * #updates #updates *) val eq_simproc = - Simplifier.simproc_global @{theory HOL} "record_eq" ["r = s"] - (fn ctxt => fn t => - (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ => - (case rec_id ~1 T of - "" => NONE - | name => - (case get_equalities (Proof_Context.theory_of ctxt) name of - NONE => NONE - | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) - | _ => NONE)); + Simplifier.make_simproc @{context} "record_eq" + {lhss = [@{term "r = s"}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of + Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ => + (case rec_id ~1 T of + "" => NONE + | name => + (case get_equalities (Proof_Context.theory_of ctxt) name of + NONE => NONE + | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) + | _ => NONE), + identifier = []}; (* split_simproc *) @@ -1280,9 +1291,10 @@ P t = ~1: completely split P t > 0: split up to given bound of record extensions.*) fun split_simproc P = - Simplifier.simproc_global @{theory HOL} "record_split" ["x"] - (fn ctxt => fn t => - (case t of + Simplifier.make_simproc @{context} "record_split" + {lhss = [@{term x}], + proc = fn _ => fn ctxt => fn ct => + (case Thm.term_of ct of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => if quantifier = @{const_name Pure.all} orelse quantifier = @{const_name All} orelse @@ -1291,7 +1303,7 @@ (case rec_id ~1 T of "" => NONE | _ => - let val split = P t in + let val split = P (Thm.term_of ct) in if split <> 0 then (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of NONE => NONE @@ -1305,13 +1317,16 @@ else NONE end) else NONE - | _ => NONE)); + | _ => NONE), + identifier = []}; val ex_sel_eq_simproc = - Simplifier.simproc_global @{theory HOL} "ex_sel_eq" ["Ex t"] - (fn ctxt => fn t => + Simplifier.make_simproc @{context} "ex_sel_eq" + {lhss = [@{term "Ex t"}], + proc = fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; fun mkeq (lr, Teq, (sel, Tsel), x) i = if is_selector thy sel then let @@ -1344,7 +1359,8 @@ addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) end handle TERM _ => NONE) | _ => NONE) - end); + end, + identifier = []}; (* split_simp_tac *) diff -r 92858a52e45b -r 497eb43a3064 src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/HOL/Word/WordBitwise.thy Wed Sep 09 21:51:44 2015 +0200 @@ -497,8 +497,8 @@ text {* Tactic definition *} ML {* - -structure Word_Bitwise_Tac = struct +structure Word_Bitwise_Tac = +struct val word_ss = simpset_of @{theory_context Word}; @@ -523,10 +523,9 @@ end | _ => NONE; -val expand_upt_simproc = Simplifier.make_simproc - {lhss = [@{cpat "upt _ _"}], - name = "expand_upt", identifier = [], - proc = K upt_conv}; +val expand_upt_simproc = + Simplifier.make_simproc @{context} "expand_upt" + {lhss = [@{term "upt x y"}], proc = K upt_conv, identifier = []}; fun word_len_simproc_fn ctxt ct = case Thm.term_of ct of @@ -540,10 +539,9 @@ handle TERM _ => NONE | TYPE _ => NONE) | _ => NONE; -val word_len_simproc = Simplifier.make_simproc - {lhss = [@{cpat "len_of _"}], - name = "word_len", identifier = [], - proc = K word_len_simproc_fn}; +val word_len_simproc = + Simplifier.make_simproc @{context} "word_len" + {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn, identifier = []}; (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2, or just 5 (discarding nat) when n_sucs = 0 *) @@ -567,10 +565,10 @@ |> mk_meta_eq |> SOME end handle TERM _ => NONE; -fun nat_get_Suc_simproc n_sucs cts = Simplifier.make_simproc - {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts, - name = "nat_get_Suc", identifier = [], - proc = K (nat_get_Suc_simproc_fn n_sucs)}; +fun nat_get_Suc_simproc n_sucs ts = + Simplifier.make_simproc @{context} "nat_get_Suc" + {lhss = map (fn t => t $ @{term "n :: nat"}) ts, + proc = K (nat_get_Suc_simproc_fn n_sucs), identifier = []}; val no_split_ss = simpset_of (put_simpset HOL_ss @{context} @@ -601,10 +599,10 @@ rev_bl_order_simps} addsimprocs [expand_upt_simproc, nat_get_Suc_simproc 4 - [@{cpat replicate}, @{cpat "takefill ?x"}, - @{cpat drop}, @{cpat "bin_to_bl"}, - @{cpat "takefill_last ?x"}, - @{cpat "drop_nonempty ?x"}]], + [@{term replicate}, @{term "takefill x"}, + @{term drop}, @{term "bin_to_bl"}, + @{term "takefill_last x"}, + @{term "drop_nonempty x"}]], put_simpset no_split_ss @{context} addsimps @{thms xor3_simps carry_simps if_bool_simps} ]) diff -r 92858a52e45b -r 497eb43a3064 src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Wed Sep 09 21:51:44 2015 +0200 @@ -37,16 +37,14 @@ functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): - sig - val proc: Proof.context -> term -> thm option - end -= + sig val proc: Proof.context -> cterm -> thm option end = struct (*the simplification procedure*) -fun proc ctxt t = +fun proc ctxt ct = let val prems = Simplifier.prems_of ctxt; + val t = Thm.term_of ct; val ([t'], ctxt') = Variable.import_terms true [t] ctxt val export = singleton (Variable.export ctxt' ctxt) (* FIXME ctxt vs. ctxt' *) diff -r 92858a52e45b -r 497eb43a3064 src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Wed Sep 09 21:51:44 2015 +0200 @@ -44,7 +44,7 @@ signature CANCEL_NUMERALS = sig - val proc: Proof.context -> term -> thm option + val proc: Proof.context -> cterm -> thm option end; functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS = @@ -65,9 +65,10 @@ in seek terms1 end; (*the simplification procedure*) -fun proc ctxt t = +fun proc ctxt ct = let val prems = Simplifier.prems_of ctxt + val t = Thm.term_of ct val ([t'], ctxt') = Variable.import_terms true [t] ctxt val export = singleton (Variable.export ctxt' ctxt) (* FIXME ctxt vs. ctxt' (!?) *) diff -r 92858a52e45b -r 497eb43a3064 src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Wed Sep 09 21:51:44 2015 +0200 @@ -38,7 +38,7 @@ functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): sig - val proc: Proof.context -> term -> thm option + val proc: Proof.context -> cterm -> thm option end = struct @@ -65,8 +65,9 @@ | NONE => find_repeated (tab, t::past, terms); (*the simplification procedure*) -fun proc ctxt t = +fun proc ctxt ct = let + val t = Thm.term_of ct val ([t'], ctxt') = Variable.import_terms true [t] ctxt val export = singleton (Variable.export ctxt' ctxt) (* FIXME ctxt vs. ctxt' (!?) *) diff -r 92858a52e45b -r 497eb43a3064 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Sep 09 21:51:44 2015 +0200 @@ -87,7 +87,7 @@ sig val prems_lin_arith_tac: Proof.context -> int -> tactic val lin_arith_tac: Proof.context -> int -> tactic - val lin_arith_simproc: Proof.context -> term -> thm option + val lin_arith_simproc: Proof.context -> cterm -> thm option val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, neqE: thm list, simpset: simpset, @@ -775,7 +775,7 @@ let val thms = maps LA_Logic.atomize (Simplifier.prems_of ctxt) val Hs = map Thm.prop_of thms - val Tconcl = LA_Logic.mk_Trueprop concl + val Tconcl = LA_Logic.mk_Trueprop (Thm.term_of concl) in case prove ctxt [] false Hs Tconcl of (* concl provable? *) (split_neq, SOME js) => prover ctxt thms Tconcl js split_neq true diff -r 92858a52e45b -r 497eb43a3064 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Wed Sep 09 21:51:44 2015 +0200 @@ -168,8 +168,9 @@ ML_Lex.read_source false source |> ML_Context.expression (Input.range_of source) "proc" "Morphism.morphism -> Proof.context -> cterm -> thm option" - ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ - \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ + ("Context.map_proof (Simplifier.define_simproc_cmd " ^ + ML_Syntax.atomic (ML_Syntax.make_binding name) ^ + "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") |> Context.proof_map; diff -r 92858a52e45b -r 497eb43a3064 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Pure/pure_thy.ML Wed Sep 09 21:51:44 2015 +0200 @@ -176,11 +176,6 @@ #> Sign.add_syntax (Symbol.xsymbolsN, true) [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), - ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\_", [4, 0], 3)), - ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), - ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\", 2)), (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), diff -r 92858a52e45b -r 497eb43a3064 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Pure/raw_simplifier.ML Wed Sep 09 21:51:44 2015 +0200 @@ -35,10 +35,10 @@ safe_solvers: string list} type simproc val eq_simproc: simproc * simproc -> bool + val cert_simproc: theory -> string -> + {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} + -> simproc val transform_simproc: morphism -> simproc -> simproc - val make_simproc: {name: string, lhss: cterm list, - proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} -> simproc - val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc val simpset_of: Proof.context -> simpset val put_simpset: simpset -> Proof.context -> Proof.context val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset @@ -105,10 +105,6 @@ val solver: Proof.context -> solver -> int -> tactic val simp_depth_limit_raw: Config.raw val default_mk_sym: Proof.context -> thm -> thm option - val simproc_global_i: theory -> string -> term list -> - (Proof.context -> term -> thm option) -> simproc - val simproc_global: theory -> string -> string list -> - (Proof.context -> term -> thm option) -> simproc val simp_trace_depth_limit_raw: Config.raw val simp_trace_raw: Config.raw val simp_debug_raw: Config.raw @@ -675,6 +671,10 @@ fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2); +fun cert_simproc thy name {lhss, proc, identifier} = + Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, + id = (stamp (), map Thm.trim_context identifier)}; + fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) = Simproc {name = name, @@ -682,19 +682,6 @@ proc = Morphism.transform phi proc, id = (s, Morphism.fact phi ths)}; -fun make_simproc {name, lhss, proc, identifier} = - Simproc {name = name, lhss = map Thm.term_of lhss, proc = proc, - id = (stamp (), map Thm.trim_context identifier)}; - -fun mk_simproc name lhss proc = - make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct => - proc ctxt (Thm.term_of ct), identifier = []}; - -(* FIXME avoid global thy and Logic.varify_global *) -fun simproc_global_i thy name = mk_simproc name o map (Thm.global_cterm_of thy o Logic.varify_global); -fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy); - - local fun add_proc (proc as Proc {name, lhs, ...}) ctxt = diff -r 92858a52e45b -r 497eb43a3064 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Pure/simplifier.ML Wed Sep 09 21:51:44 2015 +0200 @@ -36,12 +36,11 @@ val cong_del: attribute val check_simproc: Proof.context -> xstring * Position.T -> string val the_simproc: Proof.context -> string -> simproc - val def_simproc: {name: binding, lhss: term list, - proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} -> - local_theory -> local_theory - val def_simproc_cmd: {name: binding, lhss: string list, - proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} -> - local_theory -> local_theory + type 'a simproc_spec = + {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} + val make_simproc: Proof.context -> string -> term simproc_spec -> simproc + val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory + val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory val pretty_simpset: bool -> Proof.context -> Pretty.T val default_mk_sym: Proof.context -> thm -> thm option val prems_of: Proof.context -> thm list @@ -61,10 +60,6 @@ val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context type trace_ops val set_trace_ops: trace_ops -> theory -> theory - val simproc_global_i: theory -> string -> term list -> - (Proof.context -> term -> thm option) -> simproc - val simproc_global: theory -> string -> string list -> - (Proof.context -> term -> thm option) -> simproc val rewrite: Proof.context -> conv val asm_rewrite: Proof.context -> conv val full_rewrite: Proof.context -> conv @@ -122,19 +117,25 @@ (* define simprocs *) +type 'a simproc_spec = + {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}; + +fun make_simproc ctxt name {lhss, proc, identifier} = + let + val ctxt' = fold Variable.auto_fixes lhss ctxt; + val lhss' = Variable.export_terms ctxt' ctxt lhss; + in + cert_simproc (Proof_Context.theory_of ctxt) name + {lhss = lhss', proc = proc, identifier = identifier} + end; + local -fun gen_simproc prep {name = b, lhss, proc, identifier} lthy = +fun def_simproc prep b {lhss, proc, identifier} lthy = let - val simproc = make_simproc - {name = Local_Theory.full_name lthy b, - lhss = - let - val lhss' = prep lthy lhss; - val ctxt' = fold Variable.auto_fixes lhss' lthy; - in Variable.export_terms ctxt' lthy lhss' end |> map (Thm.cterm_of lthy), - proc = proc, - identifier = identifier}; + val simproc = + make_simproc lthy (Local_Theory.full_name lthy b) + {lhss = prep lthy lhss, proc = proc, identifier = identifier}; in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => let @@ -149,8 +150,8 @@ in -val def_simproc = gen_simproc Syntax.check_terms; -val def_simproc_cmd = gen_simproc Syntax.read_terms; +val define_simproc = def_simproc Syntax.check_terms; +val define_simproc_cmd = def_simproc Syntax.read_terms; end; diff -r 92858a52e45b -r 497eb43a3064 src/Tools/induct.ML --- a/src/Tools/induct.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/Tools/induct.ML Wed Sep 09 21:51:44 2015 +0200 @@ -158,8 +158,10 @@ | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); val rearrange_eqs_simproc = - Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"] - (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t)); + Simplifier.make_simproc @{context} "rearrange_eqs" + {lhss = [@{term "Pure.all(t)"}], + proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct, + identifier = []}; (* rotate k premises to the left by j, skipping over first j premises *) diff -r 92858a52e45b -r 497eb43a3064 src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Wed Sep 09 17:07:51 2015 +0200 +++ b/src/ZF/Datatype_ZF.thy Wed Sep 09 21:51:44 2015 +0200 @@ -70,8 +70,9 @@ val datatype_ss = simpset_of @{context}; - fun proc ctxt old = - let val thy = Proof_Context.theory_of ctxt + fun proc ctxt ct = + let val old = Thm.term_of ct + val thy = Proof_Context.theory_of ctxt val _ = if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old) else () @@ -104,7 +105,9 @@ handle Match => NONE; - val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; + val conv = + Simplifier.make_simproc @{context} "data_free" + {lhss = [@{term "(x::i) = y"}], proc = K proc, identifier = []}; end; \ diff -r 92858a52e45b -r 497eb43a3064 src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/ZF/arith_data.ML Wed Sep 09 21:51:44 2015 +0200 @@ -76,9 +76,6 @@ (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE) end; -fun prep_simproc thy (name, pats, proc) = - Simplifier.simproc_global thy name pats proc; - (*** Use CancelNumerals simproc without binary numerals, just for cancellation ***) @@ -202,22 +199,24 @@ val nat_cancel = - map (prep_simproc @{theory}) - [("nateq_cancel_numerals", - ["l #+ m = n", "l = m #+ n", - "l #* m = n", "l = m #* n", - "succ(m) = n", "m = succ(n)"], - EqCancelNumerals.proc), - ("natless_cancel_numerals", - ["l #+ m < n", "l < m #+ n", - "l #* m < n", "l < m #* n", - "succ(m) < n", "m < succ(n)"], - LessCancelNumerals.proc), - ("natdiff_cancel_numerals", - ["(l #+ m) #- n", "l #- (m #+ n)", - "(l #* m) #- n", "l #- (m #* n)", - "succ(m) #- n", "m #- succ(n)"], - DiffCancelNumerals.proc)]; + [Simplifier.make_simproc @{context} "nateq_cancel_numerals" + {lhss = + [@{term "l #+ m = n"}, @{term "l = m #+ n"}, + @{term "l #* m = n"}, @{term "l = m #* n"}, + @{term "succ(m) = n"}, @{term "m = succ(n)"}], + proc = K EqCancelNumerals.proc, identifier = []}, + Simplifier.make_simproc @{context} "natless_cancel_numerals" + {lhss = + [@{term "l #+ m < n"}, @{term "l < m #+ n"}, + @{term "l #* m < n"}, @{term "l < m #* n"}, + @{term "succ(m) < n"}, @{term "m < succ(n)"}], + proc = K LessCancelNumerals.proc, identifier = []}, + Simplifier.make_simproc @{context} "natdiff_cancel_numerals" + {lhss = + [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"}, + @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"}, + @{term "succ(m) #- n"}, @{term "m #- succ(n)"}], + proc = K DiffCancelNumerals.proc, identifier = []}]; end; diff -r 92858a52e45b -r 497eb43a3064 src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Wed Sep 09 17:07:51 2015 +0200 +++ b/src/ZF/int_arith.ML Wed Sep 09 21:51:44 2015 +0200 @@ -146,9 +146,6 @@ val int_mult_minus_simps = [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2]; -fun prep_simproc thy (name, pats, proc) = - Simplifier.simproc_global thy name pats proc; - structure CancelNumeralsCommon = struct val mk_sum = (fn _ : typ => mk_sum) @@ -210,22 +207,24 @@ ); val cancel_numerals = - map (prep_simproc @{theory}) - [("inteq_cancel_numerals", - ["l $+ m = n", "l = m $+ n", - "l $- m = n", "l = m $- n", - "l $* m = n", "l = m $* n"], - EqCancelNumerals.proc), - ("intless_cancel_numerals", - ["l $+ m $< n", "l $< m $+ n", - "l $- m $< n", "l $< m $- n", - "l $* m $< n", "l $< m $* n"], - LessCancelNumerals.proc), - ("intle_cancel_numerals", - ["l $+ m $<= n", "l $<= m $+ n", - "l $- m $<= n", "l $<= m $- n", - "l $* m $<= n", "l $<= m $* n"], - LeCancelNumerals.proc)]; + [Simplifier.make_simproc @{context} "inteq_cancel_numerals" + {lhss = + [@{term "l $+ m = n"}, @{term "l = m $+ n"}, + @{term "l $- m = n"}, @{term "l = m $- n"}, + @{term "l $* m = n"}, @{term "l = m $* n"}], + proc = K EqCancelNumerals.proc, identifier = []}, + Simplifier.make_simproc @{context} "intless_cancel_numerals" + {lhss = + [@{term "l $+ m $< n"}, @{term "l $< m $+ n"}, + @{term "l $- m $< n"}, @{term "l $< m $- n"}, + @{term "l $* m $< n"}, @{term "l $< m $* n"}], + proc = K LessCancelNumerals.proc, identifier = []}, + Simplifier.make_simproc @{context} "intle_cancel_numerals" + {lhss = + [@{term "l $+ m $<= n"}, @{term "l $<= m $+ n"}, + @{term "l $- m $<= n"}, @{term "l $<= m $- n"}, + @{term "l $* m $<= n"}, @{term "l $<= m $* n"}], + proc = K LeCancelNumerals.proc, identifier = []}]; (*version without the hyps argument*) @@ -268,8 +267,9 @@ structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); val combine_numerals = - prep_simproc @{theory} - ("int_combine_numerals", ["i $+ j", "i $- j"], CombineNumerals.proc); + Simplifier.make_simproc @{context} "int_combine_numerals" + {lhss = [@{term "i $+ j"}, @{term "i $- j"}], + proc = K CombineNumerals.proc, identifier = []}; @@ -314,8 +314,8 @@ structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); val combine_numerals_prod = - prep_simproc @{theory} - ("int_combine_numerals_prod", ["i $* j"], CombineNumeralsProd.proc); + Simplifier.make_simproc @{context} "int_combine_numerals_prod" + {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc, identifier = []}; end;