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