38140
|
1 |
(* Title: HOL/Subst/Unifier.thy
|
1476
|
2 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
968
|
3 |
Copyright 1993 University of Cambridge
|
|
4 |
|
|
5 |
*)
|
|
6 |
|
38140
|
7 |
header {* Definition of Most General Unifier *}
|
15635
|
8 |
|
|
9 |
theory Unifier
|
|
10 |
imports Subst
|
|
11 |
begin
|
968
|
12 |
|
24823
|
13 |
definition
|
38140
|
14 |
Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
|
|
15 |
where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
|
968
|
16 |
|
24823
|
17 |
definition
|
38140
|
18 |
MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool" (infixr ">>" 52)
|
|
19 |
where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
|
968
|
20 |
|
24823
|
21 |
definition
|
38140
|
22 |
MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
|
|
23 |
where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
|
968
|
24 |
|
24823
|
25 |
definition
|
|
26 |
Idem :: "('a * 'a uterm)list => bool" where
|
|
27 |
"Idem s \<longleftrightarrow> (s <> s) =$= s"
|
15635
|
28 |
|
|
29 |
|
|
30 |
lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
|
|
31 |
|
|
32 |
|
38140
|
33 |
subsection {* Unifiers *}
|
15635
|
34 |
|
|
35 |
lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
|
24823
|
36 |
by (simp add: Unifier_def)
|
15635
|
37 |
|
|
38 |
|
38140
|
39 |
lemma Cons_Unifier: "v \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> Unifier ((v, r) #s) t u"
|
24823
|
40 |
by (simp add: Unifier_def repl_invariance)
|
15635
|
41 |
|
|
42 |
|
38140
|
43 |
subsection {* Most General Unifiers *}
|
15635
|
44 |
|
|
45 |
lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
|
24823
|
46 |
by (simp add: unify_defs eq_commute)
|
15635
|
47 |
|
|
48 |
|
|
49 |
lemma MoreGen_Nil [iff]: "[] >> s"
|
24823
|
50 |
by (auto simp add: MoreGeneral_def)
|
15635
|
51 |
|
|
52 |
lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"
|
24823
|
53 |
apply (unfold unify_defs)
|
|
54 |
apply (auto intro: ssubst_subst2 subst_comp_Nil)
|
|
55 |
done
|
15635
|
56 |
|
24823
|
57 |
lemma MGUnifier_Var [intro!]: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
|
|
58 |
apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
|
|
59 |
apply safe
|
|
60 |
apply (rule exI)
|
|
61 |
apply (erule subst, rule Cons_trivial [THEN subst_sym])
|
|
62 |
apply (erule ssubst_subst2)
|
|
63 |
apply (simp (no_asm_simp) add: Var_not_occs)
|
|
64 |
done
|
15635
|
65 |
|
|
66 |
|
38140
|
67 |
subsection {* Idempotence *}
|
15635
|
68 |
|
38140
|
69 |
lemma Idem_Nil [iff]: "Idem []"
|
24823
|
70 |
by (simp add: Idem_def)
|
15635
|
71 |
|
38140
|
72 |
lemma Idem_iff: "Idem s = (sdom s Int srange s = {})"
|
24823
|
73 |
by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
|
15635
|
74 |
|
38140
|
75 |
lemma Var_Idem [intro!]: "~ (Var v <: t) ==> Idem [(v,t)]"
|
24823
|
76 |
by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
|
15635
|
77 |
|
|
78 |
lemma Unifier_Idem_subst:
|
38140
|
79 |
"Idem(r) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
|
|
80 |
Unifier (r <> s) (t <| r) (u <| r)"
|
24823
|
81 |
by (simp add: Idem_def Unifier_def comp_subst_subst)
|
15635
|
82 |
|
|
83 |
lemma Idem_comp:
|
38140
|
84 |
"Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
|
|
85 |
(!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
|
|
86 |
Idem (r <> s)"
|
24823
|
87 |
apply (frule Unifier_Idem_subst, blast)
|
|
88 |
apply (force simp add: Idem_def subst_eq_iff)
|
|
89 |
done
|
15635
|
90 |
|
968
|
91 |
end
|