Theory Match_Cterm_Ex

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Match_Cterm_Ex
  imports 
    AutoCorres2.Match_Cterm
   
begin

section ‹ML Antiquotation to Match and Morph›

text ‹The following example illustrates how to define a localized ‹simproc› and properly morph
the formal entities to accomodate the interpretations. Note that the ‹simproc› is a
‹declaration› and hence a similar approach might be useful for declarations in general›

declare [[verbose=5]]
locale two_eq =
  fixes f g ::"'a ⇒ 'b" 
  assumes eq: "f = g"
begin
lemma swap: "(f x = g x) ≡ (g x = f x)"
  by (simp add: eq)

simproc_setup swap_simproc (‹f x = g y›) = ‹
fn phi => fn ctxt => fn ct => 
  let 
    val _ = tracing ("swap_simproc: " ^ @{make_string} ct)
    val {x, ...} = @{cterm_morph_match (fo) ‹f ?x = g ?x›} phi ct ― ‹the pattern is morphed›
    val _ = tracing ("match for x: " ^ @{make_string} x) 
    val swap = Morphism.thm phi @{thm swap}  ― ‹the theorem is morphed an instantiated›
             |> Drule.infer_instantiate' ctxt [SOME x]
    val _ = tracing ("swap instantiated: " ^ @{make_string} swap)
  in SOME swap  end
  handle Pattern.MATCH => (tracing "match failed"; NONE)
›

end

definition "F ≡ (λ_::int. 1::nat)"
definition "G ≡ (λ_::int. 1::nat)"


interpretation F_G: two_eq F G
  by (unfold_locales) (simp add: F_def G_def)

lemma "F a = G a"
  apply simp ― ‹The interpreted pattern is matched by ‹morph_match››
  apply (simp add: F_G.eq)
  done

lemma "F a = G b"
  apply simp? ― ‹Matching fails because \<^term>‹a› and \<^term>‹b› are not the same›
  oops

lemma "G a = F a"
  apply simp? ― ‹Already the pattern match of the ‹simproc_setup› fails here, because the
                  equation has the wrong order. So the ‹simproc› is not even invoked›
  oops
declare [[verbose=0]]

end