--- 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 "\<Colon>" 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*)
--- 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 \<open>
-let
- val typ = Simple_Syntax.read_typ;
-in
- Sign.del_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
-end
-\<close>
+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]]
--- 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 "\<Colon>"},
- which actually looks exactly the same in some {\LaTeX} styles.
-
\item Dummy variables (written as underscore) may occur in different
roles.
--- 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 "\<exists>x. ?P x"}],
- name = "reduce_ex_simproc",
- proc = K proc,
- identifier = []};
+ Simplifier.make_simproc @{context} "reduce_ex_simproc"
+ {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
end;
--- 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 \<open>
fn _ => Induct.map_simpset (fn ss => ss
addsimprocs
- [Simplifier.simproc_global @{theory} "swap_induct_false"
- ["induct_false \<Longrightarrow> PROP P \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> PROP P \<Longrightarrow> 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 \<Longrightarrow> 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 \<open>
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 = []}])
\<close>
--- 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
--- 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 ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [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
--- 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 \<open>K Int_Arith.setup\<close>
simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
- "(m::'a::linordered_idom) <= n" |
+ "(m::'a::linordered_idom) \<le> n" |
"(m::'a::linordered_idom) = n") =
- \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
+ \<open>K Lin_Arith.simproc\<close>
subsection\<open>More Inequality Reasoning\<close>
--- 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) \<le> n"}, @{term "(m::real) = n"}],
+ proc = K Lin_Arith.simproc, identifier = []}
(* setup *)
--- 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) \<le> n"}, @{term "(m::int) = n"}],
+ proc = K Lin_Arith.simproc, identifier = []},
+ Simplifier.make_simproc @{context} "antisym_le"
+ {lhss = [@{term "(x::'a::order) \<le> y"}],
+ proc = K prove_antisym_le, identifier = []},
+ Simplifier.make_simproc @{context} "antisym_less"
+ {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
+ proc = K prove_antisym_less, identifier = []}])
structure Simpset = Generic_Data
(
--- 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" ("_\<Colon>_" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_\<Colon>_" [4, 0] 3)
-
-syntax (xsymbols output)
- "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_ \<Colon> _" [4, 0] 3)
+syntax (output)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
(* sorts as intersections *)
--- 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 *}
--- 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 \<open>Lin_Arith.global_setup\<close>
declaration \<open>K Lin_Arith.setup\<close>
-simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
- \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
+simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
+ \<open>K Lin_Arith.simproc\<close>
(* 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
--- 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 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
+ Simplifier.make_simproc @{context} "perm_simp"
+ {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc', identifier = []};
fun projections ctxt rule =
Project_Rule.projections ctxt rule
--- 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);
--- 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);
--- 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 _\<sharp>_, then try the simplifier",
+ | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, 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";
--- 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 = (\<Sum> (x, y)\<leftarrow>zip v w. x * y)"
-definition mv :: "('a \<Colon> semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+definition mv :: "('a :: semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> '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 \<Colon> semiring_0) list"
+ fixes v :: "('a :: semiring_0) list"
assumes "length w = length v"
shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w"
(is "(\<Sum>x\<leftarrow>_. ?f x) = _")
@@ -317,11 +317,11 @@
*)
definition [simp]: "unzip w = (map fst w, map snd w)"
-primrec insert :: "('a \<Rightarrow> 'b \<Colon> linorder) => 'a \<Rightarrow> 'a list => 'a list" where
+primrec insert :: "('a \<Rightarrow> 'b :: linorder) => 'a \<Rightarrow> '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 \<Rightarrow> 'b \<Colon> linorder) \<Rightarrow> 'a list => 'a list" where
+primrec sort :: "('a \<Rightarrow> 'b :: linorder) \<Rightarrow> 'a list => 'a list" where
"sort f [] = []" |
"sort f (x # xs) = insert f x (sort f xs)"
--- 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 \<open>
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 = []}])
\<close>
--- 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"}))
\<close>
--- 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" ("_ \<Colon> _" [4, 0] 3)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
(*>*)
chapter {* HOL-\SPARK{} Reference *}
--- 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;
--- 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;
--- 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
--- 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
--- 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) \<le> n"}, @{term "(m::real) = n"}],
+ proc = K Lin_Arith.simproc, identifier = []}
(* setup *)
--- 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) \<le> n"}, @{term "(m::int) = n"}],
+ proc = K Lin_Arith.simproc, identifier = []},
+ Simplifier.make_simproc @{context} "antisym_le"
+ {lhss = [@{term "(x::'a::order) \<le> y"}],
+ proc = K prove_antisym_le, identifier = []},
+ Simplifier.make_simproc @{context} "antisym_less"
+ {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
+ proc = K prove_antisym_less, identifier = []}])
structure Simpset = Generic_Data
(
--- 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])
--- 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 =
--- 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) \<le> 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}))
--- 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
--- 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 ***)
--- 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 \<le> c"},
+ @{term "c < (a::'a::{field,ord}) / b"},
+ @{term "c \<le> (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;
-
--- 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 *)
--- 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}
])
--- 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' *)
--- 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' (!?) *)
--- 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' (!?) *)
--- 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
--- 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;
--- 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 ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
- ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
(const "Pure.eq", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
(const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
--- 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 =
--- 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;
--- 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 *)
--- 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;
\<close>
--- 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;
--- 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;