section \Matching First-Order Terms - Soundness and Completeness\
text \
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.
\
theory Project_Matching
imports Main
begin
subsection \Terms and Substitutions\
text \
First-order terms are either variables or function symbols applied to a list of
argument terms:
\
type_synonym id = string
datatype "term" = Var id | Fun id "term list"
text \
A substitution is a mapping from variables to terms.
\
type_synonym subst = "id \ term option"
text \
Define a function \subst\ that applies a substitution to a given term.
Variables that are not part of the substitution should be left untouched.
\
fun subst :: "subst \ term \ term"
where
"subst \ t = undefined"
text \
Define a function \vars\ that computes the set of variables occurring in a given term.
\
fun vars :: "term \ id set"
where
"vars t = undefined"
text \
Define a matching algorithm that, given two lists of terms \ts\ and \us\, and an initial
substitution \\\, computes (if possible) a substitution \\\ that makes the \ts\ equal to \us\:
\map (subst \) ts = us\
\
fun match :: "term list \ term list \ subst \ subst option"
where
"match ts us \ = undefined"
text \
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 \\\ with the variables occurring in \ts\.
\
lemma match_Some_dom:
assumes "match ts us \ = Some \"
shows "dom \ \ dom \ \ \(set (map vars ts))"
sorry
subsection \Soundness\
text \
Prove that \match\ is sound.
You will need an auxiliary result on the relationship between the initial substitution \\\ and
the resulting substitution \\\. To this end the order @{term "(\\<^sub>m)"} should be useful.
\
lemma match_sound:
assumes "match ts us \ = Some \"
shows "map (subst \) ts = us"
sorry
subsection \Matchers\
text \
Define the set of matchers of two given lists of terms \ts\ and \us\.
Here, a matcher for \ts\ and \us\ is any substitution \\\ that makes \ts\ equal to \us\ and is
defined at least on all variables of \ts\.
\
definition matchers :: "term list \ term list \ subst set"
where
"matchers ts us = undefined"
text \
Prove the following equations for @{const matchers} (after suitably replacing \whatever\).
\
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 \ length us \ matchers ts us = whatever"
"length ss = length us \ matchers (ss @ ts) (us @ vs) = whatever"
sorry
subsection \Completeness\
text \
Prove that @{const match} is complete, that is, if \match ts us \ = None\ then there is
no extension of \\\ that is a matcher of \ts\ and \us\.
\
lemma match_complete:
assumes "match ts us \ = None"
shows "matchers ts us \ {\. \ \\<^sub>m \} = {}"
sorry
end