(* Author: Christian Sternagel <c.sternagel@gmail.com> Author: René Thiemann <rene.thiemann@uibk.ac.at> License: LGPL *) section ‹Matching› theory Matching imports Abstract_Matching Unification (* for decompose *) begin function match_term_list where "match_term_list [] σ = Some σ" | "match_term_list ((Var x, t) # P) σ = (if σ x = None ∨ σ x = Some t then match_term_list P (σ (x ↦ t)) else None)" | "match_term_list ((Fun f ss, Fun g ts) # P) σ = (case decompose (Fun f ss) (Fun g ts) of None ⇒ None | Some us ⇒ match_term_list (us @ P) σ)" | "match_term_list ((Fun f ss, Var x) # P) σ = None" by (pat_completeness) auto termination by (standard, rule wf_inv_image [OF wf_measure [of size_mset], of "mset ∘ fst"]) (auto simp: pair_size_def) lemma match_term_list_Some_matchrel: assumes "match_term_list P σ = Some τ" shows "((mset P, σ), ({#}, τ)) ∈ matchrel⇧^{*}" using assms proof (induction P σ rule: match_term_list.induct) case (2 x t P σ) from "2.prems" have *: "σ x = None ∨ σ x = Some t" and **: "match_term_list P (σ (x ↦ t)) = Some τ" by (auto split: if_splits) from MATCH1.Var [of σ x t "mset P", OF *] have "((mset ((Var x, t) # P), σ), (mset P, σ (x ↦ t))) ∈ matchrel⇧^{*}" by (simp add: MATCH1_matchrel_conv) with "2.IH" [OF * **] show ?case by (blast dest: rtrancl_trans) next case (3 f ss g ts P σ) let ?s = "Fun f ss" and ?t = "Fun g ts" from "3.prems" have [simp]: "f = g" and *: "length ss = length ts" and **: "decompose ?s ?t = Some (zip ss ts)" "match_term_list (zip ss ts @ P) σ = Some τ" by (auto split: option.splits) from MATCH1.Fun [OF *, of "mset P" g σ] have "((mset ((?s, ?t) # P), σ), (mset (zip ss ts @ P), σ)) ∈ matchrel⇧^{*}" by (simp add: MATCH1_matchrel_conv ac_simps) with "3.IH" [OF **] show ?case by (blast dest: rtrancl_trans) qed simp_all lemma match_term_list_None: assumes "match_term_list P σ = None" shows "matchers_map σ ∩ matchers (set P) = {}" using assms proof (induction P σ rule: match_term_list.induct) case (2 x t P σ) have "¬ (σ x = None ∨ σ x = Some t) ∨ (σ x = None ∨ σ x = Some t) ∧ match_term_list P (σ (x ↦ t)) = None" using "2.prems" by (auto split: if_splits) then show ?case proof assume *: "¬ (σ x = None ∨ σ x = Some t)" have "¬ (∃y. (({#(Var x, t)#}, σ), y) ∈ matchrel)" proof presume "¬ ?thesis" then obtain y where "MATCH1 ({#(Var x, t)#}, σ) y" by (auto simp: MATCH1_matchrel_conv) then show False using * by (cases) simp_all qed simp moreover have "(({#(Var x, t)#}, σ), ({#(Var x, t)#}, σ)) ∈ matchrel⇧^{*}" by simp ultimately have "(({#(Var x, t)#}, σ), ({#(Var x, t)#}, σ)) ∈ matchrel⇧^{!}" by (metis NF_I normalizability_I) from irreducible_reachable_imp_matchers_empty [OF this] have "matchers_map σ ∩ matchers {(Var x, t)} = {}" by simp then show ?case by auto next presume *: "σ x = None ∨ σ x = Some t" and "match_term_list P (σ (x ↦ t)) = None" from "2.IH" [OF this] have "matchers_map (σ (x ↦ t)) ∩ matchers (set P) = {}" . with MATCH1_matchers [OF MATCH1.Var [of σ x, OF *], of "mset P"] show ?case by simp qed auto next case (3 f ss g ts P σ) let ?s = "Fun f ss" and ?t = "Fun g ts" have "decompose ?s ?t = None ∨ decompose ?s ?t = Some (zip ss ts) ∧ match_term_list (zip ss ts @ P) σ = None" using "3.prems" by (auto split: option.splits) then show ?case proof assume "decompose ?s ?t = None" then show ?case by auto next presume "decompose ?s ?t = Some (zip ss ts)" and "match_term_list (zip ss ts @ P) σ = None" from "3.IH" [OF this] show ?case by auto qed auto qed simp_all text ‹Compute a matching substitution for a list of term pairs @{term P}, where left-hand sides are "patterns" against which the right-hand sides are matched.› definition match_list :: "('v ⇒ ('f, 'w) term) ⇒ (('f, 'v) term × ('f, 'w) term) list ⇒ ('f, 'v, 'w) gsubst option" where "match_list d P = map_option (subst_of_map d) (match_term_list P Map.empty)" lemma match_list_sound: assumes "match_list d P = Some σ" shows "σ ∈ matchers (set P)" using matchrel_sound [of "mset P"] and match_term_list_Some_matchrel [of P Map.empty] and assms by (auto simp: match_list_def) lemma match_list_matches: assumes "match_list d P = Some σ" shows "⋀p t. (p, t) ∈ set P ⟹ p ⋅ σ = t" using match_list_sound [OF assms] by (force simp: matchers_def) lemma match_list_complete: assumes "match_list d P = None" shows "matchers (set P) = {}" using match_term_list_None [of P Map.empty] and assms by (simp add: match_list_def) lemma match_list_None_conv: "match_list d P = None ⟷ matchers (set P) = {}" using match_list_sound [of d P] and match_list_complete [of d P] by (metis empty_iff not_None_eq) definition "match t l = match_list Var [(l, t)]" lemma match_sound: assumes "match t p = Some σ" shows "σ ∈ matchers {(p, t)}" using match_list_sound [of Var "[(p, t)]"] and assms by (simp add: match_def) lemma match_matches: assumes "match t p = Some σ" shows "p ⋅ σ = t" using match_sound [OF assms] by (force simp: matchers_def) lemma match_complete: assumes "match t p = None" shows "matchers {(p, t)} = {}" using match_list_complete [of Var "[(p, t)]"] and assms by (simp add: match_def) definition matches :: "('f, 'w) term ⇒ ('f, 'v) term ⇒ bool" where "matches t p = (case match_list (λ _. t) [(p,t)] of None ⇒ False | Some _ ⇒ True)" lemma matches_iff: "matches t p ⟷ (∃σ. p ⋅ σ = t)" using match_list_sound [of _ "[(p,t)]"] and match_list_complete [of _ "[(p,t)]"] unfolding matches_def matchers_def by (force simp: split: option.splits) lemma match_complete': assumes "p ⋅ σ = t" shows "∃τ. match t p = Some τ ∧ (∀x∈vars_term p. σ x = τ x)" proof - from assms have σ: "σ ∈ matchers {(p,t)}" by (simp add: matchers_def) with match_complete[of t p] obtain τ where match: "match t p = Some τ" by (auto split: option.splits) from match_sound[OF this] have "τ ∈ matchers {(p, t)}" . from matchers_vars_term_eq[OF σ this] match show ?thesis by auto qed abbreviation lvars :: "(('f, 'v) term × ('f, 'w) term) list ⇒ 'v set" where "lvars P ≡ ⋃ ((vars_term ∘ fst) ` set P)" lemma match_list_complete': assumes "⋀s t. (s, t) ∈ set P ⟹ s ⋅ σ = t" shows "∃τ. match_list d P = Some τ ∧ (∀x∈lvars P. σ x = τ x)" proof - from assms have "σ ∈ matchers (set P)" by (force simp: matchers_def) moreover with match_list_complete [of d P] obtain τ where "match_list d P = Some τ" by auto moreover with match_list_sound [of d P] have "τ ∈ matchers (set P)" by (auto simp: match_def split: option.splits) ultimately show ?thesis using matchers_vars_term_eq [of σ "set P" "τ"] by auto qed end