2 Author: Alexander Krauss, Technische Universitaet Muenchen |
2 Author: Alexander Krauss, Technische Universitaet Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* Case study: Unification Algorithm *} |
5 header {* Case study: Unification Algorithm *} |
6 |
6 |
7 (*<*)theory Unification |
7 theory Unification |
8 imports Main |
8 imports Main |
9 begin(*>*) |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 This is a formalization of a first-order unification |
12 This is a formalization of a first-order unification |
13 algorithm. It uses the new "function" package to define recursive |
13 algorithm. It uses the new "function" package to define recursive |
14 functions, which allows a better treatment of nested recursion. |
14 functions, which allows a better treatment of nested recursion. |
15 |
15 |
16 This is basically a modernized version of a previous formalization |
16 This is basically a modernized version of a previous formalization |
17 by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on |
17 by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on |
18 previous work by Paulson and Manna @{text "&"} Waldinger (for details, see |
18 previous work by Paulson and Manna \& Waldinger (for details, see |
19 there). |
19 there). |
20 |
20 |
21 Unlike that formalization, where the proofs of termination and |
21 Unlike that formalization, where the proofs of termination and |
22 some partial correctness properties are intertwined, we can prove |
22 some partial correctness properties are intertwined, we can prove |
23 partial correctness and termination separately. |
23 partial correctness and termination separately. |
24 *} |
24 *} |
25 |
25 |
|
26 |
26 subsection {* Basic definitions *} |
27 subsection {* Basic definitions *} |
27 |
28 |
28 datatype 'a trm = |
29 datatype 'a trm = |
29 Var 'a |
30 Var 'a |
30 | Const 'a |
31 | Const 'a |
59 text {* Equivalence of substitutions: *} |
60 text {* Equivalence of substitutions: *} |
60 |
61 |
61 definition eqv (infix "=\<^sub>s" 50) |
62 definition eqv (infix "=\<^sub>s" 50) |
62 where |
63 where |
63 "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" |
64 "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" |
|
65 |
64 |
66 |
65 subsection {* Basic lemmas *} |
67 subsection {* Basic lemmas *} |
66 |
68 |
67 lemma apply_empty[simp]: "t \<triangleleft> [] = t" |
69 lemma apply_empty[simp]: "t \<triangleleft> [] = t" |
68 by (induct t) auto |
70 by (induct t) auto |
102 lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')" |
104 lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')" |
103 by (auto simp:eqv_def) |
105 by (auto simp:eqv_def) |
104 |
106 |
105 lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)" |
107 lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)" |
106 by auto |
108 by auto |
|
109 |
107 |
110 |
108 subsection {* Specification: Most general unifiers *} |
111 subsection {* Specification: Most general unifiers *} |
109 |
112 |
110 definition |
113 definition |
111 "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)" |
114 "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)" |