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