section \<open>Matching First-Order Terms - Soundness and Completeness\<close>

text \<open>
A matching algorithm for first-order terms computes tries to compute a substitution that
witnesses that one (list of) term(s) is an instance of another.

In this project you will implement and verify a matching algorithm.
\<close>

theory Project_Matching
  imports Main
begin

subsection \<open>Terms and Substitutions\<close>

text \<open>
First-order terms are either variables or function symbols applied to a list of
argument terms:
\<close>
type_synonym id = string
datatype "term" = Var id | Fun id "term list"

text \<open>
A substitution is a mapping from variables to terms.
\<close>
type_synonym subst = "id \<Rightarrow> term option"

text \<open>
Define a function \<open>subst\<close> that applies a substitution to a given term.
Variables that are not part of the substitution should be left untouched.
\<close>
fun subst :: "subst \<Rightarrow> term \<Rightarrow> term"
  where
    "subst \<sigma> t = undefined"

text \<open>
Define a function \<open>vars\<close> that computes the set of variables occurring in a given term.
\<close>
fun vars :: "term \<Rightarrow> id set"
  where
    "vars t = undefined"

text \<open>
Define a matching algorithm that, given two lists of terms \<open>ts\<close> and \<open>us\<close>, and an initial
substitution \<open>\<sigma>\<close>, computes (if possible) a substitution \<open>\<tau>\<close> that makes the \<open>ts\<close> equal to \<open>us\<close>:

  \<open>map (subst \<tau>) ts = us\<close>
\<close>
fun match :: "term list \<Rightarrow> term list \<Rightarrow> subst \<Rightarrow> subst option"
  where
    "match ts us \<sigma> = undefined"

text \<open>
Show that the domain @{const dom} of a substitution computed by @{const match} is contained
in the union of the domain of the initial substitution \<open>\<sigma>\<close> with the variables occurring in \<open>ts\<close>.
\<close>
lemma match_Some_dom:
  assumes "match ts us \<sigma> = Some \<tau>"
  shows "dom \<tau> \<subseteq> dom \<sigma> \<union> \<Union>(set (map vars ts))"
  sorry


subsection \<open>Soundness\<close>

text \<open>
Prove that \<open>match\<close> is sound.

You will need an auxiliary result on the relationship between the initial substitution \<open>\<sigma>\<close> and
the resulting substitution \<open>\<tau>\<close>. To this end the order @{term "(\<subseteq>\<^sub>m)"} should be useful.
\<close>
lemma match_sound:
  assumes "match ts us \<sigma> = Some \<tau>"
  shows "map (subst \<tau>) ts = us"
  sorry


subsection \<open>Matchers\<close>

text \<open>
Define the set of matchers of two given lists of terms \<open>ts\<close> and \<open>us\<close>.

Here, a matcher for \<open>ts\<close> and \<open>us\<close> is any substitution \<open>\<sigma>\<close> that makes \<open>ts\<close> equal to \<open>us\<close> and is
defined at least on all variables of \<open>ts\<close>.
\<close>
definition matchers :: "term list \<Rightarrow> term list \<Rightarrow> subst set"
  where
    "matchers ts us = undefined"

text \<open>
Prove the following equations for @{const matchers} (after suitably replacing \<open>whatever\<close>).
\<close>
lemma matchers_simp [simp]:
  "matchers [] (u # us) = whatever"
  "matchers (t # ts) [] = whatever"
  "matchers (Var x # ts) (u # us) = whatever"
  "matchers (Fun f ts # tss) (Var y # us) = whatever"
  "matchers (Fun f ts # tss) (Fun g us # uss) = whatever"
  "length ts \<noteq> length us \<Longrightarrow> matchers ts us = whatever"
  "length ss = length us \<Longrightarrow> matchers (ss @ ts) (us @ vs) = whatever"
  sorry


subsection \<open>Completeness\<close>

text \<open>
Prove that @{const match} is complete, that is, if \<open>match ts us \<sigma> = None\<close> then there is
no extension of \<open>\<sigma>\<close> that is a matcher of \<open>ts\<close> and \<open>us\<close>.
\<close>
lemma match_complete:
  assumes "match ts us \<sigma> = None"
  shows "matchers ts us \<inter> {\<tau>. \<sigma> \<subseteq>\<^sub>m \<tau>} = {}"
  sorry

end