# HG changeset patch
# User wenzelm
# Date 1469046970 -7200
# Node ID b01154b743146571820d48b633b6684931457746
# Parent  847eefdca90d6b333f33b8001ceeae08690776b4
provide Pure.simp/simp_all, which only know about meta-equality;

diff -r 847eefdca90d -r b01154b74314 NEWS
--- 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 ***
 
diff -r 847eefdca90d -r b01154b74314 src/Doc/Isar_Ref/Generic.thy
--- 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>
 
 
diff -r 847eefdca90d -r b01154b74314 src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- 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
diff -r 847eefdca90d -r b01154b74314 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- 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
diff -r 847eefdca90d -r b01154b74314 src/Pure/simplifier.ML
--- 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;