# Theory Separation_Logic_Imperative_HOL.Syntax_Match

```section ‹Syntactic Matching in the Simplifier›
theory Syntax_Match
imports Main
begin

subsection ‹Non-Matching›

text ‹
We define the predicates ‹syntax_nomatch›
and ‹syntax_fo_nomatch›. The expression
‹syntax_nomatch pattern object› is simplified to true only if
the term ‹pattern› syntactically matches the term ‹object›.
Note that, semantically, ‹syntax_nomatch pattern object› is always
true. While ‹syntax_nomatch› does higher-order matching,
‹syntax_fo_nomatch› does first-order matching.

The intended application of these predicates are as guards for simplification
rules, enforcing additional syntactic restrictions on the applicability of
the simplification rule.
›
definition syntax_nomatch :: "'a ⇒ 'b ⇒ bool"
where syntax_nomatch_def: "syntax_nomatch pat obj ≡ True"
definition syntax_fo_nomatch :: "'a ⇒ 'b ⇒ bool"
where syntax_fo_nomatch_def: "syntax_fo_nomatch pat obj ≡ True"

(* Prevent simplifier to simplify inside syntax_xx predicates *)
lemma [cong]: "syntax_fo_nomatch x y = syntax_fo_nomatch x y" by simp
lemma [cong]: "syntax_nomatch x y = syntax_nomatch x y" by simp

ML ‹
structure Syntax_Match = struct
val nomatch_thm = @{thm syntax_nomatch_def};
val fo_nomatch_thm = @{thm syntax_fo_nomatch_def};

fun fo_nomatch_simproc ctxt credex = let
(*val ctxt = Simplifier.the_context ss;*)
val thy = Proof_Context.theory_of ctxt;

val redex = Thm.term_of credex;
val (_,[pat,obj]) = strip_comb redex;

fun fo_matches po = (Pattern.first_order_match
thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;
in
if fo_matches (pat,obj) then NONE else SOME fo_nomatch_thm
end

fun nomatch_simproc ctxt credex = let
(*val ctxt = Simplifier.the_context ss;*)
val thy = Proof_Context.theory_of ctxt;

val redex = Thm.term_of credex;
val (_,[pat,obj]) = strip_comb redex;
in
if Pattern.matches thy (pat,obj) then NONE else SOME nomatch_thm
end
end
›
simproc_setup nomatch ("syntax_nomatch pat obj")
= ‹K Syntax_Match.nomatch_simproc›
simproc_setup fo_nomatch ("syntax_fo_nomatch pat obj")
= ‹K Syntax_Match.fo_nomatch_simproc›

subsection ‹Examples›
subsubsection ‹Ordering AC-structures›
text ‹
Currently, the simplifier rules for ac-rewriting only work when
associativity groups to the right. Here, we define rules that work for
associativity grouping to the left. They are useful for operators where
syntax is parsed (and pretty-printed) left-associative.
›

locale ac_operator =
fixes f
assumes right_assoc: "f (f a b) c = f a (f b c)"
assumes commute: "f a b = f b a"
begin
lemmas left_assoc = right_assoc[symmetric]
lemma left_commute: "f a (f b c) = f b (f a c)"
done

lemmas right_ac = right_assoc left_commute commute

lemma right_commute: "f (f a b) c = f (f a c) b"

lemma safe_commute: "syntax_fo_nomatch (f x y) a ⟹ f a b = f b a"

lemmas left_ac = left_assoc right_commute safe_commute
end

interpretation mult: ac_operator "(*) ::'a::ab_semigroup_mult ⇒ _ ⇒ _"
apply unfold_locales
done