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 (metis (no_types, lifting) case_prodD)
      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 fastforce
      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 fastforce

      have "closed_except u {||}"
        using u inner (name, irs) |∈| rs
        by fastforce
      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 fastforce
        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 (metis (no_types, lifting) case_prodD)

  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 (metis (no_types, lifting) case_prodD)

  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