move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
authorhoelzl
Fri Oct 24 15:07:49 2014 +0200 (2014-10-24)
changeset 587759cd64a66a765
parent 58774 d6435f0bf966
child 58776 95e58e04e534
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
NEWS
src/HOL/HOL.thy
     1.1 --- a/NEWS	Thu Oct 23 16:25:08 2014 +0200
     1.2 +++ b/NEWS	Fri Oct 24 15:07:49 2014 +0200
     1.3 @@ -49,6 +49,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Add NO_MATCH-simproc, allows to check for syntactic non-equality
     1.8 +
     1.9  * Generalized and consolidated some theorems concerning divsibility:
    1.10    dvd_reduce ~> dvd_add_triv_right_iff
    1.11    dvd_plus_eq_right ~> dvd_add_right_iff
     2.1 --- a/src/HOL/HOL.thy	Thu Oct 23 16:25:08 2014 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Oct 24 15:07:49 2014 +0200
     2.3 @@ -1701,6 +1701,29 @@
     2.4  ML_file "Tools/cnf.ML"
     2.5  
     2.6  
     2.7 +section {* @{text NO_MATCH} simproc *}
     2.8 +
     2.9 +text {*
    2.10 + The simplification procedure can be used to avoid simplification of terms of a certain form
    2.11 +*}
    2.12 +
    2.13 +definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
    2.14 +lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
    2.15 +
    2.16 +simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
    2.17 +  let
    2.18 +    val thy = Proof_Context.theory_of ctxt
    2.19 +    val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
    2.20 +    val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
    2.21 +  in if m then NONE else SOME @{thm NO_MATCH_def} end
    2.22 +*}
    2.23 +
    2.24 +text {*
    2.25 +  This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
    2.26 +  is only applied, if the pattern @{term pat} does not match the value @{term val}.
    2.27 +*}
    2.28 +
    2.29 +
    2.30  subsection {* Code generator setup *}
    2.31  
    2.32  subsubsection {* Generic code generator preprocessor setup *}