# HG changeset patch
# User nipkow
# Date 1442827916 -7200
# Node ID 9e37178084c52bb591f2f7451f63c3b9da7d84ec
# Parent  94efa2688ff6b8c9b52df0e61f02f6dd5011957a
Added new simplifier predicate ASSUMPTION

diff -r 94efa2688ff6 -r 9e37178084c5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Sep 19 22:32:26 2015 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 21 11:31:56 2015 +0200
@@ -1691,6 +1691,32 @@
 \<close>
 
 
+text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+not to simplify the argument and to solve it by an assumption. *}
+
+definition ASSUMPTION :: "bool \<Rightarrow> bool" where
+"ASSUMPTION A \<equiv> A"
+
+lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
+by (rule refl)
+
+lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
+by(simp add: ASSUMPTION_def)
+
+lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
+by(simp add: ASSUMPTION_def)
+
+setup {*
+let
+  val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
+    resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
+    resolve_tac ctxt (Simplifier.prems_of ctxt))
+in
+  map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
+end
+*}
+
+
 subsection \<open>Code generator setup\<close>
 
 subsubsection \<open>Generic code generator preprocessor setup\<close>