Theory Rewriting_Pterm

subsection ‹Pure pattern matching rule sets›

theory Rewriting_Pterm
imports Rewriting_Pterm_Elim
begin

type_synonym prule = "name × pterm"

primrec prule :: "prule ⇒ bool" where
"prule (_, rhs) ⟷ wellformed rhs ∧ closed rhs ∧ is_abs rhs"

lemma pruleI[intro!]: "wellformed rhs ⟹ closed rhs ⟹ is_abs rhs ⟹ prule (name, rhs)"
by simp

locale prules = constants C_info "fst |`| rs" for C_info and rs :: "prule fset" +
  assumes all_rules: "fBall rs prule"
  assumes fmap: "is_fmap rs"
  assumes not_shadows: "fBall rs (λ(_, rhs). ¬ shadows_consts rhs)"
  assumes welldefined_rs: "fBall rs (λ(_, rhs). welldefined rhs)"

subsubsection ‹Rewriting›

inductive prewrite :: "prule fset ⇒ pterm ⇒ pterm ⇒ bool" ("_/ ⊢⇩p/ _ ⟶/ _" [50,0,50] 50) for rs where
step: "(name, rhs) |∈| rs ⟹ rs ⊢⇩p Pconst name ⟶ rhs" |
beta: "c |∈| cs ⟹ c ⊢ t → t' ⟹ rs ⊢⇩p Pabs cs $⇩p t ⟶ t'" |
"fun": "rs ⊢⇩p t ⟶ t' ⟹ rs ⊢⇩p t $⇩p u ⟶ t' $⇩p u" |
arg: "rs ⊢⇩p u ⟶ u' ⟹ rs ⊢⇩p t $⇩p u ⟶ t $⇩p u'"

global_interpretation prewrite: rewriting "prewrite rs" for rs
by standard (auto intro: prewrite.intros simp: app_pterm_def)+

abbreviation prewrite_rt :: "prule fset ⇒ pterm ⇒ pterm ⇒ bool" ("_/ ⊢⇩p/ _ ⟶*/ _" [50,0,50] 50) where
"prewrite_rt rs ≡ (prewrite rs)⇧*⇧*"

subsubsection ‹Translation from @{typ irule_set} to @{typ "prule fset"}›

definition finished :: "irule_set ⇒ bool" where
"finished rs = fBall rs (λ(_, irs). arity irs = 0)"

definition translate_rhs :: "irules ⇒ pterm" where
"translate_rhs = snd ∘ fthe_elem"

definition compile :: "irule_set ⇒ prule fset" where
"compile = fimage (map_prod id translate_rhs)"

lemma compile_heads: "fst |`| compile rs = fst |`| rs"
unfolding compile_def by simp

subsubsection ‹Correctness of translation›

lemma arity_zero_shape:
  assumes "arity_compatibles rs" "arity rs = 0" "is_fmap rs" "rs ≠ {||}"
  obtains t where "rs = {| ([], t) |}"
proof -
  from assms obtain ppats prhs where "(ppats, prhs) |∈| rs"
    by fast

  moreover {
    fix pats rhs
    assume "(pats, rhs) |∈| rs"
    with assms have "length pats = 0"
      by (metis arity_compatible_length)
    hence "pats = []"
      by simp
  }
  note all = this

  ultimately have proto: "([], prhs) |∈| rs" by auto

  have "fBall rs (λ(pats, rhs). pats = [] ∧ rhs = prhs)"
    proof safe
      fix pats rhs
      assume cur: "(pats, rhs) |∈| rs"
      with all show "pats = []" .
      with cur have "([], rhs) |∈| rs" by auto

      with proto show "rhs = prhs"
        using assms by (auto dest: is_fmapD)
    qed
  hence "fBall rs (λr. r = ([], prhs))"
    by blast
  with assms have "rs = {| ([], prhs) |}"
    by (simp add: singleton_fset_is)
  thus thesis
    by (rule that)
qed

lemma (in irules) compile_rules:
  assumes "finished rs"
  shows "prules C_info (compile rs)"
proof
  show "is_fmap (compile rs)"
    using fmap
    unfolding compile_def map_prod_def id_apply
    by (rule is_fmap_image)
next
  show "fdisjnt (fst |`| compile rs) C"
    unfolding compile_def
    using disjnt by simp
next
  have
    "fBall (compile rs) prule"
    "fBall (compile rs) (λ(_, rhs). ¬ shadows_consts rhs)"
    "fBall (compile rs) (λ(_, rhs). welldefined rhs)"
    proof (safe del: fsubsetI)
      fix name rhs
      assume "(name, rhs) |∈| compile rs" (* FIXME clone of compile_correct *)
      then obtain irs where "(name, irs) |∈| rs" "rhs = translate_rhs irs"
        unfolding compile_def by force
      hence "is_fmap irs" "irs ≠ {||}" "arity irs = 0"
        using assms inner unfolding finished_def by blast+
      moreover have "arity_compatibles irs"
        using ‹(name, irs) |∈| rs› inner by (blast dest: fpairwiseD)
      ultimately obtain u where "irs = {| ([], u) |}"
        by (metis arity_zero_shape)
      hence "rhs = u" and u: "([], u) |∈| irs"
        unfolding ‹rhs = _› translate_rhs_def by simp+
      hence "abs_ish [] u"
        using inner ‹(name, irs) |∈| rs› by blast
      thus "is_abs rhs"
        unfolding abs_ish_def ‹rhs = u› by simp

      show "wellformed rhs"
        using u ‹(name, irs) |∈| rs› inner unfolding ‹rhs = u›
        by blast

      have "closed_except u {||}"
        using u inner ‹(name, irs) |∈| rs›
        by (metis (mono_tags, lifting) case_prod_conv fbspec freess_empty)
      thus "closed rhs"
        unfolding ‹rhs = u› .

      {
        assume "shadows_consts rhs"
        hence "shadows_consts u"
          unfolding compile_def ‹rhs = u› by simp
        moreover have "¬ shadows_consts u"
          using inner ‹([], u) |∈| irs› ‹(name, irs) |∈| rs› by blast
        ultimately show False by blast
      }

      have "welldefined u"
        using fbspec[OF inner ‹(name, irs) |∈| rs›, simplified] ‹([], u) |∈| irs›
        by blast
      thus "welldefined rhs"
        unfolding ‹rhs = u› compile_def
        by simp
    qed
  thus
    "fBall (compile rs) prule"
    "fBall (compile rs) (λ(_, rhs). ¬ pre_constants.shadows_consts C_info (fst |`| compile rs) rhs)"
    "fBall (compile rs) (λ(_, rhs). pre_constants.welldefined C_info (fst |`| compile rs) rhs)"
    unfolding compile_heads by auto
next
  show "distinct all_constructors"
    by (fact distinct_ctr)
qed

theorem (in irules) compile_correct:
  assumes "compile rs ⊢⇩p t ⟶ t'" "finished rs"
  shows "rs ⊢⇩i t ⟶ t'"
using assms(1) proof induction
  case (step name rhs)
  then obtain irs where "rhs = translate_rhs irs" "(name, irs) |∈| rs"
    unfolding compile_def by force
  hence "arity_compatibles irs"
    using inner by (blast dest: fpairwiseD)

  have "is_fmap irs" "irs ≠ {||}" "arity irs = 0"
    using assms inner ‹(name, irs) |∈| rs› unfolding finished_def by blast+
  then obtain u where "irs = {| ([], u) |}"
    using ‹arity_compatibles irs›
    by (metis arity_zero_shape)

  show ?case
    unfolding ‹rhs = _›
    apply (rule irewrite.step)
      apply fact
    unfolding ‹irs = _› translate_rhs_def irewrite_step_def
    by (auto simp: const_term_def)
qed (auto intro: irewrite.intros)

theorem (in irules) compile_complete:
  assumes "rs ⊢⇩i t ⟶ t'" "finished rs"
  shows "compile rs ⊢⇩p t ⟶ t'"
using assms(1) proof induction
  case (step name irs params rhs t t')
  hence "arity_compatibles irs"
    using inner by (blast dest: fpairwiseD)

  have "is_fmap irs" "irs ≠ {||}" "arity irs = 0"
    using assms inner step unfolding finished_def by blast+
  then obtain u where "irs = {| ([], u) |}"
    using ‹arity_compatibles irs›
    by (metis arity_zero_shape)
  with step have "name, [], u ⊢⇩i t → t'"
    by simp
  hence "t = Pconst name"
    unfolding irewrite_step_def
    by (cases t) (auto split: if_splits simp: const_term_def)
  hence "t' = u"
    using ‹name, [], u ⊢⇩i t → t'›
    unfolding irewrite_step_def
    by (cases t) (auto split: if_splits simp: const_term_def)

  have "(name, t') |∈| compile rs"
    unfolding compile_def
    proof
      show "(name, t') = map_prod id translate_rhs (name, irs)"
        using ‹irs = _› ‹t' = u›
        by (simp add: split_beta translate_rhs_def)
    qed fact
  thus ?case
    unfolding ‹t = _›
    by (rule prewrite.step)
qed (auto intro: prewrite.intros)

export_code
  compile finished
  checking Scala

end