--- a/NEWS Wed Jul 20 21:26:11 2016 +0200
+++ b/NEWS Wed Jul 20 22:36:10 2016 +0200
@@ -52,6 +52,11 @@
* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.
+* Pure provides basic versions of proof methods "simp" and "simp_all"
+that only know about meta-equality (==). Potential INCOMPATIBILITY in
+theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
+is relevant to avoid confusion of Pure.simp vs. HOL.simp.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Generic.thy Wed Jul 20 21:26:11 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Jul 20 22:36:10 2016 +0200
@@ -258,6 +258,8 @@
\begin{tabular}{rcll}
@{method_def simp} & : & \<open>method\<close> \\
@{method_def simp_all} & : & \<open>method\<close> \\
+ \<open>Pure.\<close>@{method_def (Pure) simp} & : & \<open>method\<close> \\
+ \<open>Pure.\<close>@{method_def (Pure) simp_all} & : & \<open>method\<close> \\
@{attribute_def simp_depth_limit} & : & \<open>attribute\<close> & default \<open>100\<close> \\
\end{tabular}
\<^medskip>
@@ -354,6 +356,12 @@
\end{tabular}
\end{center}
+
+ \<^medskip>
+ In Isabelle/Pure, proof methods @{method (Pure) simp} and @{method (Pure)
+ simp_all} only know about meta-equality \<open>\<equiv>\<close>. Any new object-logic needs to
+ re-define these methods via @{ML Simplifier.method_setup} in ML:
+ Isabelle/FOL or Isabelle/HOL may serve as blue-prints.
\<close>
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Wed Jul 20 21:26:11 2016 +0200
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Wed Jul 20 22:36:10 2016 +0200
@@ -82,7 +82,7 @@
assumes "\<bottom>"
shows A
proof -
- from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
+ from \<open>\<bottom>\<close> have "\<forall>A. A" by (simp only: false_def)
then show A ..
qed
@@ -108,7 +108,7 @@
assumes "\<not> A" and A
shows B
proof -
- from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
+ from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" by (simp only: not_def)
from this and \<open>A\<close> have "\<bottom>" ..
then show B ..
qed
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Wed Jul 20 21:26:11 2016 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Wed Jul 20 22:36:10 2016 +0200
@@ -7,8 +7,8 @@
theory Adhoc_Overloading_Examples
imports
Main
+ "~~/src/HOL/Library/Infinite_Set"
"~~/src/Tools/Adhoc_Overloading"
- "~~/src/HOL/Library/Infinite_Set"
begin
text \<open>Adhoc overloading allows to overload a constant depending on
--- a/src/Pure/simplifier.ML Wed Jul 20 21:26:11 2016 +0200
+++ b/src/Pure/simplifier.ML Wed Jul 20 22:36:10 2016 +0200
@@ -69,7 +69,10 @@
val simp_modifiers': Method.modifier parser list
val simp_modifiers: Method.modifier parser list
val method_setup: Method.modifier parser list -> theory -> theory
- val easy_setup: thm -> thm list -> theory -> theory
+ val unsafe_solver_tac: Proof.context -> int -> tactic
+ val unsafe_solver: solver
+ val safe_solver_tac: Proof.context -> int -> tactic
+ val safe_solver: solver
end;
structure Simplifier: SIMPLIFIER =
@@ -376,31 +379,22 @@
(CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
"simplification (all goals)";
-fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn ctxt0 =>
- let
- val trivialities = Drule.reflexive_thm :: trivs;
-
- fun unsafe_solver_tac ctxt =
- FIRST' [resolve_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
- val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
-
- (*no premature instantiation of variables during simplification*)
- fun safe_solver_tac ctxt =
- FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
- val safe_solver = mk_solver "easy safe" safe_solver_tac;
+fun unsafe_solver_tac ctxt =
+ FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
+val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
- fun mk_eq thm =
- if can Logic.dest_equals (Thm.concl_of thm) then [thm]
- else [thm RS reflect] handle THM _ => [];
+(*no premature instantiation of variables during simplification*)
+fun safe_solver_tac ctxt =
+ FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+val safe_solver = mk_solver "Pure safe" safe_solver_tac;
- fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
- in
- empty_simpset ctxt0
- setSSolver safe_solver
- setSolver unsafe_solver
- |> set_subgoaler asm_simp_tac
- |> set_mksimps (K mksimps)
- end));
+val _ =
+ Theory.setup
+ (method_setup [] #> Context.theory_map (map_ss (fn ctxt =>
+ empty_simpset ctxt
+ setSSolver safe_solver
+ setSolver unsafe_solver
+ |> set_subgoaler asm_simp_tac)));
end;