Theory Pats

chapter ‹Wellformedness of patterns›

theory Pats
imports Term
begin

text ‹
  The @{class term} class already defines a generic definition of ‹matching› a ‹pattern› with a
  term. Importantly, the type of patterns is neither generic, nor a dedicated pattern type; instead,
  it is @{typ term} itself.

  Patterns are a proper subset of terms, with the restriction that no abstractions may occur and
  there must be at most a single occurrence of any variable (usually known as ‹linearity›).
  The first restriction can be modelled in a datatype, the second cannot. Consequently, I define a
  predicate that captures both properties.

  Using linearity, many more generic properties can be proved, for example that substituting the
  environment produced by matching yields the matched term.
›

fun linear :: "term  bool" where
"linear (Free _)  True" |
"linear (Const _)  True" |
"linear (t1 $ t2)  linear t1  linear t2  ¬ is_free t1  fdisjnt (frees t1) (frees t2)" |
"linear _  False"

lemmas linear_simps[simp] =
  linear.simps(2)[folded const_term_def]
  linear.simps(3)[folded app_term_def]

lemma linear_implies_no_abs: "linear t  no_abs t"
proof induction
  case Const
  then show ?case
    by (fold const_term_def free_term_def app_term_def) auto
next
  case Free
  then show ?case
    by (fold const_term_def free_term_def app_term_def) auto
next
  case App
  then show ?case
    by (fold const_term_def free_term_def app_term_def) auto
qed auto

fun linears :: "term list  bool" where
"linears []  True" |
"linears (t # ts)  linear t  fdisjnt (frees t) (freess ts)  linears ts"

lemma linears_butlastI[intro]: "linears ts  linears (butlast ts)"
proof (induction ts)
  case (Cons t ts)
  hence "linear t" "linears (butlast ts)"
    by simp+
  moreover have " fdisjnt (frees t) (freess (butlast ts))"
    proof (rule fdisjnt_subset_right)
      show "freess (butlast ts) |⊆| freess ts"
        by (rule freess_subset) (auto dest: in_set_butlastD)
    next
      show "fdisjnt (frees t) (freess ts)"
        using Cons by simp
    qed
  ultimately show ?case
    by simp
qed simp

lemma linears_appI[intro]:
  assumes "linears xs" "linears ys" "fdisjnt (freess xs) (freess ys)"
  shows "linears (xs @ ys)"
using assms proof (induction xs)
  case (Cons z zs)
  hence "linears zs"
    by simp+

  have "fdisjnt (frees z) (freess zs |∪| freess ys)"
    proof (rule fdisjnt_union_right)
      show "fdisjnt (frees z) (freess zs)"
        using linears (z # zs) by simp
    next
      have "frees z |⊆| freess (z # zs)"
        unfolding freess_def by simp
      thus "fdisjnt (frees z) (freess ys)"
        by (rule fdisjnt_subset_left) fact
    qed

  moreover have "linears (zs @ ys)"
    proof (rule Cons)
      show "fdisjnt (freess zs) (freess ys)"
        using Cons
        by (auto intro: freess_subset fdisjnt_subset_left)
    qed fact+

  ultimately show ?case
    using Cons by auto
qed simp

lemma linears_linear: "linears ts  t  set ts  linear t"
by (induct ts) auto

lemma linears_singleI[intro]: "linear t  linears [t]"
by (simp add: freess_def fdisjnt_alt_def)

lemma linear_strip_comb: "linear t  linear (fst (strip_comb t))"
by (induction t rule: strip_comb_induct) (auto simp: split_beta)

lemma linears_strip_comb: "linear t  linears (snd (strip_comb t))"
proof (induction t rule: strip_comb_induct)
  case (app t1 t2)
  have "linears (snd (strip_comb t1) @ [t2])"
    proof (intro linears_appI linears_singleI)
      have "freess (snd (strip_comb t1)) |⊆| frees t1"
        by (subst frees_strip_comb) auto
      moreover have "fdisjnt (frees t1) (frees t2)"
        using app by auto
      ultimately have "fdisjnt (freess (snd (strip_comb t1))) (frees t2)"
        by (rule fdisjnt_subset_left)
      thus "fdisjnt (freess (snd (strip_comb t1))) (freess [t2])"
        by simp
    next
      show "linear t2" "linears (snd (strip_comb t1))"
        using app by auto
    qed
  thus ?case
    by (simp add: split_beta)
qed auto

lemma linears_appendD:
  assumes "linears (xs @ ys)"
  shows "linears xs" "linears ys" "fdisjnt (freess xs) (freess ys)"
using assms proof (induction xs)
  case (Cons x xs)
  assume "linears ((x # xs) @ ys)"

  hence "linears (x # (xs @ ys))"
    by simp
  hence "linears (xs @ ys)" "linear x" "fdisjnt (frees x) (freess (xs @ ys))"
    by auto
  hence "linears xs"
    using Cons by simp
  moreover have "fdisjnt (frees x) (freess xs)"
    proof (rule fdisjnt_subset_right)
      show "freess xs |⊆| freess (xs @ ys)" by simp
    qed fact
  ultimately show "linears (x # xs)"
    using linear x by auto

  have "fdisjnt (freess xs) (freess ys)"
    by (rule Cons) fact
  moreover have "fdisjnt (frees x) (freess ys)"
    proof (rule fdisjnt_subset_right)
      show "freess ys |⊆| freess (xs @ ys)" by simp
    qed fact
  ultimately show "fdisjnt (freess (x # xs)) (freess ys)"
    unfolding fdisjnt_alt_def
    by auto
qed (auto simp: fdisjnt_alt_def)

lemma linear_list_comb:
  assumes "linear f" "linears xs" "fdisjnt (frees f) (freess xs)" "¬ is_free f"
  shows "linear (list_comb f xs)"
using assms
proof (induction xs arbitrary: f)
  case (Cons x xs)

  hence *: "fdisjnt (frees f) (frees x |∪| freess xs)"
    by simp

  have "linear (list_comb (f $ x) xs)"
    proof (rule Cons)
      have "linear x"
        using Cons by simp
      moreover have "fdisjnt (frees f) (frees x)"
        using * by (auto intro: fdisjnt_subset_right)
      ultimately show "linear (f $ x)"
        using assms Cons by simp
    next
      show "linears xs"
        using Cons by simp
    next
      have "fdisjnt (frees f) (freess xs)"
        using * by (auto intro: fdisjnt_subset_right)
      moreover have "fdisjnt (frees x) (freess xs)"
        using Cons by simp
      ultimately show "fdisjnt (frees (f $ x)) (freess xs)"
        by (auto intro: fdisjnt_union_left)
    qed auto
  thus ?case
    by (simp add: app_term_def)
qed auto

corollary linear_list_comb': "linears xs  linear (name $$ xs)"
by (auto intro: linear_list_comb simp: fdisjnt_alt_def)

lemma linear_strip_comb_cases[consumes 1]:
  assumes "linear pat"
  obtains (comb) s args where "strip_comb pat = (Const s, args)" "pat = s $$ args"
        | (free) s where "strip_comb pat = (Free s, [])" "pat = Free s"
using assms
proof (induction pat rule: strip_comb_induct)
  case (app t1 t2)
  show ?case
    proof (rule "app.IH")
      show "linear t1"
        using app by simp
    next
      fix s
      assume "strip_comb t1 = (Free s, [])"
      hence "t1 = Free s"
        by (metis fst_conv snd_conv strip_comb_empty)
      hence False
        using app by simp
      thus thesis
        by simp
    next
      fix s args
      assume "strip_comb t1 = (Const s, args)"
      with app show thesis
        by (fastforce simp add: strip_comb_app)
    qed
next
  case (no_app t)
  thus ?case
    by (cases t) (auto simp: const_term_def)
qed

lemma wellformed_linearI: "linear t  wellformed' n t"
by (induct t) auto

lemma pat_cases:
  obtains (free) s where "t = Free s"
        | (comb) name args where "linears args" "t = name $$ args"
        | (nonlinear) "¬ linear t"
proof (cases t)
  case Free
  thus thesis using free by simp
next
  case Bound
  thus thesis using nonlinear by simp
next
  case Abs
  thus thesis using nonlinear by simp
next
  case (Const name)
  have "linears []" by simp
  moreover have "t = name $$ []" unfolding Const by (simp add: const_term_def)
  ultimately show thesis
    by (rule comb)
next
  case (App u v)
  show thesis
    proof (cases "linear t")
      case False
      thus thesis using nonlinear by simp
    next
      case True
      thus thesis
        proof (cases rule: linear_strip_comb_cases)
          case free
          thus thesis using that by simp
        next
          case (comb name args)
          moreover hence "linears (snd (strip_comb t))"
            using True by (blast intro: linears_strip_comb)
          ultimately have "linears args"
            by simp
          thus thesis using that comb by simp
        qed
    qed
qed

corollary linear_pat_cases[consumes 1]:
  assumes "linear t"
  obtains (free) s where "t = Free s"
        | (comb) name args where "linears args" "t = name $$ args"
using assms
by (metis pat_cases)

lemma linear_pat_induct[consumes 1, case_names free comb]:
  assumes "linear t"
  assumes "s. P (Free s)"
  assumes "name args. linears args  (arg. arg  set args  P arg)  P (name $$ args)"
  shows "P t"
using wf_measure[of size] linear t
proof (induction t)
  case (less t)

  show ?case
    using linear t
    proof (cases rule: linear_pat_cases)
      case (free name)
      thus ?thesis
        using assms by simp
    next
      case (comb name args)
      show ?thesis
        proof (cases "args = []")
          case True
          thus ?thesis
            using assms comb by fastforce
        next
          case False
          show ?thesis
            unfolding t = _
            proof (rule assms)
              fix arg
              assume "arg  set args"

              then have "(arg, t)  measure size"
                unfolding t = _
                by (induction args) auto

              moreover have "linear arg"
                using arg  set args linears args
                by (auto dest: linears_linear)

              ultimately show "P arg"
                using less by auto
            qed fact
        qed
    qed
qed

context begin

private lemma match_subst_correctness0:
  assumes "linear t"
  shows "case match t u of
          None  (env. subst (convert_term t) env  u) |
          Some env  subst (convert_term t) env = u"
using assms proof (induction t arbitrary: u)
  case Free
  show ?case
    unfolding match.simps
    by (fold free_term_def) auto
next
  case Const
  show ?case
    unfolding match.simps
    by (fold const_term_def) (auto split: option.splits)
next
  case (App t1 t2)
  hence linear: "linear t1" "linear t2" "fdisjnt (frees t1) (frees t2)"
    by simp+

  show ?case
    proof (cases "unapp u")
      case None
      then show ?thesis
        apply simp
        apply (fold app_term_def)
        apply simp
        using app_simps(3) is_app_def by blast
    next
      case (Some u')
      then obtain u1 u2 where u: "unapp u = Some (u1, u2)" by (cases u') auto
      hence "u = app u1 u2" by auto

      note 1 = App(1)[OF linear t1, of u1]
      note 2 = App(2)[OF linear t2, of u2]

      show ?thesis
        proof (cases "match t1 u1")
          case None
          then show ?thesis
            using u
            apply simp
            apply (fold app_term_def)
            using 1 by auto
        next
          case (Some env1)
          with 1 have s1: "subst (convert_term t1) env1 = u1" by simp
          show ?thesis
            proof (cases "match t2 u2")
              case None
              then show ?thesis
                using u
                apply simp
                apply (fold app_term_def)
                using 2 by auto
            next
              case (Some env2)
              with 2 have s2: "subst (convert_term t2) env2 = u2" by simp

              note match = match t1 u1 = Some env1 match t2 u2 = Some env2

              let ?env = "env1 ++f env2"
              from match have "frees t1 = fmdom env1" "frees t2 = fmdom env2"
                by (auto simp: match_dom)
              with linear have "env1 = fmrestrict_fset (frees t1) ?env" "env2 = fmrestrict_fset (frees t2) ?env"
                apply auto
                apply (auto simp: fmfilter_alt_defs)
                apply (subst fmfilter_false; auto simp: fdisjnt_alt_def intro: fmdomI)+
                done
              with s1 s2 have "subst (convert_term t1) ?env = u1" "subst (convert_term t2) ?env = u2"
                using linear
                by (metis subst_restrict' convert_term_frees linear_implies_no_abs)+

              then show ?thesis
                using match unfolding u = _
                apply simp
                apply (fold app_term_def)
                by simp
            qed
        qed
    qed
qed auto

lemma match_subst_some[simp]:
  "match t u = Some env  linear t  subst (convert_term t) env = u"
by (metis (mono_tags) match_subst_correctness0 option.simps(5))

lemma match_subst_none:
  "match t u = None  linear t  subst (convert_term t) env = u  False"
by (metis (mono_tags, lifting) match_subst_correctness0 option.simps(4))

end

(* FIXME inverse direction? *)

lemma match_matches: "match t u = Some env  linear t  t  u"
by (metis match_subst_some linear_implies_no_abs convert_term_id matchesI)

lemma overlapping_var1I: "overlapping (Free name) t"
proof (intro overlappingI matchesI)
  show "subst (Free name) (fmap_of_list [(name, t)]) = t"
    by simp
next
  show "subst t fmempty = t"
    by simp
qed

lemma overlapping_var2I: "overlapping t (Free name)"
proof (intro overlappingI matchesI)
  show "subst (Free name) (fmap_of_list [(name, t)]) = t"
    by simp
next
  show "subst t fmempty = t"
    by simp
qed

lemma non_overlapping_appI1: "non_overlapping t1 u1  non_overlapping (t1 $ t2) (u1 $ u2)"
unfolding overlapping_def matches_def by auto

lemma non_overlapping_appI2: "non_overlapping t2 u2  non_overlapping (t1 $ t2) (u1 $ u2)"
unfolding overlapping_def matches_def by auto

lemma non_overlapping_app_constI: "non_overlapping (t1 $ t2) (Const name)"
unfolding overlapping_def matches_def by simp

lemma non_overlapping_const_appI: "non_overlapping (Const name) (t1 $ t2)"
unfolding overlapping_def matches_def by simp

lemma non_overlapping_const_constI: "x  y  non_overlapping (Const x) (Const y)"
unfolding overlapping_def matches_def by simp

lemma match_overlapping:
  assumes "linear t1" "linear t2"
  assumes "match t1 u = Some env1" "match t2 u = Some env2"
  shows "overlapping t1 t2"
proof -
  define env1' where "env1' = (fmmap convert_term env1 :: (name, term) fmap)"
  define env2' where "env2' = (fmmap convert_term env2 :: (name, term) fmap)"
  from assms have "match t1 (convert_term u :: term) = Some env1'" "match t2 (convert_term u :: term) = Some env2'"
    unfolding env1'_def env2'_def
    by (metis convert_term_match)+
  with assms show ?thesis
    by (metis overlappingI match_matches)
qed

end