src/HOL/HOL.thy
changeset 58775 9cd64a66a765
parent 58659 6c9821c32dd5
child 58826 2ed2eaabe3df
     1.1 --- a/src/HOL/HOL.thy	Thu Oct 23 16:25:08 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 24 15:07:49 2014 +0200
     1.3 @@ -1701,6 +1701,29 @@
     1.4  ML_file "Tools/cnf.ML"
     1.5  
     1.6  
     1.7 +section {* @{text NO_MATCH} simproc *}
     1.8 +
     1.9 +text {*
    1.10 + The simplification procedure can be used to avoid simplification of terms of a certain form
    1.11 +*}
    1.12 +
    1.13 +definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
    1.14 +lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
    1.15 +
    1.16 +simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
    1.17 +  let
    1.18 +    val thy = Proof_Context.theory_of ctxt
    1.19 +    val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
    1.20 +    val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
    1.21 +  in if m then NONE else SOME @{thm NO_MATCH_def} end
    1.22 +*}
    1.23 +
    1.24 +text {*
    1.25 +  This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
    1.26 +  is only applied, if the pattern @{term pat} does not match the value @{term val}.
    1.27 +*}
    1.28 +
    1.29 +
    1.30  subsection {* Code generator setup *}
    1.31  
    1.32  subsubsection {* Generic code generator preprocessor setup *}