# HG changeset patch
# User hoelzl
# Date 1414156069 -7200
# Node ID 9cd64a66a76534969ebf9f65806f24515ee3311f
# Parent  d6435f0bf9661e97adacd689d68382c5c2d332e3
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL

diff -r d6435f0bf966 -r 9cd64a66a765 NEWS
--- a/NEWS	Thu Oct 23 16:25:08 2014 +0200
+++ b/NEWS	Fri Oct 24 15:07:49 2014 +0200
@@ -49,6 +49,8 @@
 
 *** HOL ***
 
+* Add NO_MATCH-simproc, allows to check for syntactic non-equality
+
 * Generalized and consolidated some theorems concerning divsibility:
   dvd_reduce ~> dvd_add_triv_right_iff
   dvd_plus_eq_right ~> dvd_add_right_iff
diff -r d6435f0bf966 -r 9cd64a66a765 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 23 16:25:08 2014 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 24 15:07:49 2014 +0200
@@ -1701,6 +1701,29 @@
 ML_file "Tools/cnf.ML"
 
 
+section {* @{text NO_MATCH} simproc *}
+
+text {*
+ The simplification procedure can be used to avoid simplification of terms of a certain form
+*}
+
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
+lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
+
+simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
+    val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
+  in if m then NONE else SOME @{thm NO_MATCH_def} end
+*}
+
+text {*
+  This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
+  is only applied, if the pattern @{term pat} does not match the value @{term val}.
+*}
+
+
 subsection {* Code generator setup *}
 
 subsubsection {* Generic code generator preprocessor setup *}