author | haftmann |
Wed, 30 Jan 2008 10:57:44 +0100 | |
changeset 26013 | 8764a1f1253b |
parent 24444 | 448978b61556 |
child 30909 | bd4f255837e5 |
permissions | -rw-r--r-- |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, Technische Universitaet Muenchen |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
3 |
*) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
4 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
5 |
header {* Case study: Unification Algorithm *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
6 |
|
23219 | 7 |
theory Unification |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
8 |
imports Main |
23219 | 9 |
begin |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
10 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
11 |
text {* |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
12 |
This is a formalization of a first-order unification |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
13 |
algorithm. It uses the new "function" package to define recursive |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
14 |
functions, which allows a better treatment of nested recursion. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
15 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
16 |
This is basically a modernized version of a previous formalization |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
17 |
by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on |
23219 | 18 |
previous work by Paulson and Manna \& Waldinger (for details, see |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
19 |
there). |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
20 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
21 |
Unlike that formalization, where the proofs of termination and |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
22 |
some partial correctness properties are intertwined, we can prove |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
23 |
partial correctness and termination separately. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
24 |
*} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
25 |
|
23219 | 26 |
|
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
27 |
subsection {* Basic definitions *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
28 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
29 |
datatype 'a trm = |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
30 |
Var 'a |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
31 |
| Const 'a |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
32 |
| App "'a trm" "'a trm" (infix "\<cdot>" 60) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
33 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
34 |
types |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
35 |
'a subst = "('a \<times> 'a trm) list" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
36 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
37 |
text {* Applying a substitution to a variable: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
38 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
39 |
fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
40 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
41 |
"assoc x d [] = d" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
42 |
| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
43 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
44 |
text {* Applying a substitution to a term: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
45 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
46 |
fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
47 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
48 |
"(Var v) \<triangleleft> s = assoc v (Var v) s" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
49 |
| "(Const c) \<triangleleft> s = (Const c)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
50 |
| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
51 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
52 |
text {* Composition of substitutions: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
53 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
54 |
fun |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
55 |
"compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
56 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
57 |
"[] \<bullet> bl = bl" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
58 |
| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
59 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
60 |
text {* Equivalence of substitutions: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
61 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
62 |
definition eqv (infix "=\<^sub>s" 50) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
63 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
64 |
"s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
65 |
|
23219 | 66 |
|
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
67 |
subsection {* Basic lemmas *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
68 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
69 |
lemma apply_empty[simp]: "t \<triangleleft> [] = t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
70 |
by (induct t) auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
71 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
72 |
lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
73 |
by (induct \<sigma>) auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
74 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
75 |
lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
76 |
proof (induct t) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
77 |
case App thus ?case by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
78 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
79 |
case Const thus ?case by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
80 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
81 |
case (Var v) thus ?case |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
82 |
proof (induct s1) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
83 |
case Nil show ?case by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
84 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
85 |
case (Cons p s1s) thus ?case by (cases p, simp) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
86 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
87 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
88 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
89 |
lemma eqv_refl[intro]: "s =\<^sub>s s" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
90 |
by (auto simp:eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
91 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
92 |
lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
93 |
by (auto simp:eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
94 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
95 |
lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
96 |
by (auto simp:eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
97 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
98 |
lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
99 |
by (auto simp:eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
100 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
101 |
lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
102 |
by (auto simp:eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
103 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
104 |
lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
105 |
by (auto simp:eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
106 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
107 |
lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
108 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
109 |
|
23219 | 110 |
|
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
111 |
subsection {* Specification: Most general unifiers *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
112 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
113 |
definition |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
114 |
"Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
115 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
116 |
definition |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
117 |
"MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
118 |
\<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
119 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
120 |
lemma MGUI[intro]: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
121 |
"\<lbrakk>t \<triangleleft> \<sigma> = u \<triangleleft> \<sigma>; \<And>\<theta>. t \<triangleleft> \<theta> = u \<triangleleft> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>\<rbrakk> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
122 |
\<Longrightarrow> MGU \<sigma> t u" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
123 |
by (simp only:Unifier_def MGU_def, auto) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
124 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
125 |
lemma MGU_sym[sym]: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
126 |
"MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
127 |
by (auto simp:MGU_def Unifier_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
128 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
129 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
130 |
subsection {* The unification algorithm *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
131 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
132 |
text {* Occurs check: Proper subterm relation *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
133 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
134 |
fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
135 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
136 |
"occ u (Var v) = False" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
137 |
| "occ u (Const c) = False" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
138 |
| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
139 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
140 |
text {* The unification algorithm: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
141 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
142 |
function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
143 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
144 |
"unify (Const c) (M \<cdot> N) = None" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
145 |
| "unify (M \<cdot> N) (Const c) = None" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
146 |
| "unify (Const c) (Var v) = Some [(v, Const c)]" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
147 |
| "unify (M \<cdot> N) (Var v) = (if (occ (Var v) (M \<cdot> N)) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
148 |
then None |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
149 |
else Some [(v, M \<cdot> N)])" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
150 |
| "unify (Var v) M = (if (occ (Var v) M) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
151 |
then None |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
152 |
else Some [(v, M)])" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
153 |
| "unify (Const c) (Const d) = (if c=d then Some [] else None)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
154 |
| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
155 |
None \<Rightarrow> None | |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
156 |
Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
157 |
of None \<Rightarrow> None | |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
158 |
Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
159 |
by pat_completeness auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
160 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
161 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
162 |
subsection {* Partial correctness *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
163 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
164 |
text {* Some lemmas about occ and MGU: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
165 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
166 |
lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
167 |
\<Longrightarrow> t \<triangleleft> [(v,s)] = t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
168 |
by (induct t) auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
169 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
170 |
lemma MGU_Var[intro]: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
171 |
assumes no_occ: "\<not>occ (Var v) t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
172 |
shows "MGU [(v,t)] (Var v) t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
173 |
proof (intro MGUI exI) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
174 |
show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
175 |
by (cases "Var v = t", auto simp:subst_no_occ) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
176 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
177 |
fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
178 |
show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
179 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
180 |
fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
181 |
by (induct s) auto |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
182 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
183 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
184 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
185 |
declare MGU_Var[symmetric, intro] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
186 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
187 |
lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
188 |
unfolding MGU_def Unifier_def |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
189 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
190 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
191 |
text {* If unification terminates, then it computes most general unifiers: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
192 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
193 |
lemma unify_partial_correctness: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
194 |
assumes "unify_dom (M, N)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
195 |
assumes "unify M N = Some \<sigma>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
196 |
shows "MGU \<sigma> M N" |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
197 |
using assms |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
198 |
proof (induct M N arbitrary: \<sigma>) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
199 |
case (7 M N M' N' \<sigma>) -- "The interesting case" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
200 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
201 |
then obtain \<theta>1 \<theta>2 |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
202 |
where "unify M M' = Some \<theta>1" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
203 |
and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
204 |
and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
205 |
and MGU_inner: "MGU \<theta>1 M M'" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
206 |
and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
207 |
by (auto split:option.split_asm) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
208 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
209 |
show ?case |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
210 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
211 |
from MGU_inner and MGU_outer |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
212 |
have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
213 |
and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
214 |
unfolding MGU_def Unifier_def |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
215 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
216 |
thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
217 |
by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
218 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
219 |
fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
220 |
hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
221 |
and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
222 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
223 |
with MGU_inner obtain \<delta> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
224 |
where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
225 |
unfolding MGU_def Unifier_def |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
226 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
227 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
228 |
from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
229 |
by (simp add:eqv_dest[OF eqv]) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
230 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
231 |
with MGU_outer obtain \<rho> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
232 |
where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
233 |
unfolding MGU_def Unifier_def |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
234 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
235 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
236 |
have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
237 |
by (rule eqv_intro, auto simp:eqv_dest[OF eqv] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
238 |
eqv_dest[OF eqv2]) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
239 |
thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
240 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
241 |
qed (auto split:split_if_asm) -- "Solve the remaining cases automatically" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
242 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
243 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
244 |
subsection {* Properties used in termination proof *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
245 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
246 |
text {* The variables of a term: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
247 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
248 |
fun vars_of:: "'a trm \<Rightarrow> 'a set" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
249 |
where |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
250 |
"vars_of (Var v) = { v }" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
251 |
| "vars_of (Const c) = {}" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
252 |
| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
253 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
254 |
lemma vars_of_finite[intro]: "finite (vars_of t)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
255 |
by (induct t) simp_all |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
256 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
257 |
text {* Elimination of variables by a substitution: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
258 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
259 |
definition |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
260 |
"elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
261 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
262 |
lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
263 |
by (auto simp:elim_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
264 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
265 |
lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
266 |
by (auto simp:elim_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
267 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
268 |
lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
269 |
by (auto simp:elim_def eqv_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
270 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
271 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
272 |
text {* Replacing a variable by itself yields an identity subtitution: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
273 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
274 |
lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
275 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
276 |
fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
277 |
by (induct t) simp_all |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
278 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
279 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
280 |
lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
281 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
282 |
assume t_v: "t = Var v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
283 |
thus "[(v, t)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
284 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
285 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
286 |
assume id: "[(v, t)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
287 |
show "t = Var v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
288 |
proof - |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
289 |
have "t = Var v \<triangleleft> [(v, t)]" by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
290 |
also from id have "\<dots> = Var v \<triangleleft> []" .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
291 |
finally show ?thesis by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
292 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
293 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
294 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
295 |
text {* A lemma about occ and elim *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
296 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
297 |
lemma remove_var: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
298 |
assumes [simp]: "v \<notin> vars_of s" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
299 |
shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
300 |
by (induct t) simp_all |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
301 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
302 |
lemma occ_elim: "\<not>occ (Var v) t |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
303 |
\<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
304 |
proof (induct t) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
305 |
case (Var x) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
306 |
show ?case |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
307 |
proof cases |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
308 |
assume "v = x" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
309 |
thus ?thesis |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
310 |
by (simp add:var_same[symmetric]) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
311 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
312 |
assume neq: "v \<noteq> x" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
313 |
have "elim [(v, Var x)] v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
314 |
by (auto intro!:remove_var simp:neq) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
315 |
thus ?thesis .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
316 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
317 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
318 |
case (Const c) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
319 |
have "elim [(v, Const c)] v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
320 |
by (auto intro!:remove_var) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
321 |
thus ?case .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
322 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
323 |
case (App M N) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
324 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
325 |
hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
326 |
and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
327 |
and nonocc: "Var v \<noteq> M" "Var v \<noteq> N" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
328 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
329 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
330 |
from nonocc have "\<not> [(v,M)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
331 |
by (simp add:var_same[symmetric]) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
332 |
with ih1 have "elim [(v, M)] v" by blast |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
333 |
hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
334 |
hence not_in_M: "v \<notin> vars_of M" by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
335 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
336 |
from nonocc have "\<not> [(v,N)] =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
337 |
by (simp add:var_same[symmetric]) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
338 |
with ih2 have "elim [(v, N)] v" by blast |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
339 |
hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
340 |
hence not_in_N: "v \<notin> vars_of N" by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
341 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
342 |
have "elim [(v, M \<cdot> N)] v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
343 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
344 |
fix t |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
345 |
show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
346 |
proof (induct t) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
347 |
case (Var x) thus ?case by (simp add: not_in_M not_in_N) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
348 |
qed auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
349 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
350 |
thus ?case .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
351 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
352 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
353 |
text {* The result of a unification never introduces new variables: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
354 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
355 |
lemma unify_vars: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
356 |
assumes "unify_dom (M, N)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
357 |
assumes "unify M N = Some \<sigma>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
358 |
shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
359 |
(is "?P M N \<sigma> t") |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
360 |
using assms |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
361 |
proof (induct M N arbitrary:\<sigma> t) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
362 |
case (3 c v) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
363 |
hence "\<sigma> = [(v, Const c)]" by simp |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
364 |
thus ?case by (induct t) auto |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
365 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
366 |
case (4 M N v) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
367 |
hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto) |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
368 |
with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp |
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
369 |
thus ?case by (induct t) auto |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
370 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
371 |
case (5 v M) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
372 |
hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto) |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
373 |
with 5 have "\<sigma> = [(v, M)]" by simp |
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
374 |
thus ?case by (induct t) auto |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
375 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
376 |
case (7 M N M' N' \<sigma>) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
377 |
then obtain \<theta>1 \<theta>2 |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
378 |
where "unify M M' = Some \<theta>1" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
379 |
and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
380 |
and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
381 |
and ih1: "\<And>t. ?P M M' \<theta>1 t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
382 |
and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
383 |
by (auto split:option.split_asm) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
384 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
385 |
show ?case |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
386 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
387 |
fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
388 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
389 |
show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
390 |
proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M' |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
391 |
\<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'") |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
392 |
case True |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
393 |
with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
394 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
395 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
396 |
from a and ih2[where t="t \<triangleleft> \<theta>1"] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
397 |
have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
398 |
\<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
399 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
400 |
hence "v \<in> vars_of t" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
401 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
402 |
assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
403 |
with True show ?thesis by (auto dest:l) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
404 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
405 |
assume "v \<in> vars_of (t \<triangleleft> \<theta>1)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
406 |
thus ?thesis by (rule l) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
407 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
408 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
409 |
thus ?thesis by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
410 |
qed auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
411 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
412 |
qed (auto split: split_if_asm) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
413 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
414 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
415 |
text {* The result of a unification is either the identity |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
416 |
substitution or it eliminates a variable from one of the terms: *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
417 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
418 |
lemma unify_eliminates: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
419 |
assumes "unify_dom (M, N)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
420 |
assumes "unify M N = Some \<sigma>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
421 |
shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
422 |
(is "?P M N \<sigma>") |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
423 |
using assms |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
424 |
proof (induct M N arbitrary:\<sigma>) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
425 |
case 1 thus ?case by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
426 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
427 |
case 2 thus ?case by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
428 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
429 |
case (3 c v) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
430 |
have no_occ: "\<not> occ (Var v) (Const c)" by simp |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
431 |
with 3 have "\<sigma> = [(v, Const c)]" by simp |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
432 |
with occ_elim[OF no_occ] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
433 |
show ?case by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
434 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
435 |
case (4 M N v) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
436 |
hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto) |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
437 |
with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
438 |
with occ_elim[OF no_occ] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
439 |
show ?case by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
440 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
441 |
case (5 v M) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
442 |
hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto) |
24444
448978b61556
induct: proper separation of initial and terminal step;
wenzelm
parents:
23777
diff
changeset
|
443 |
with 5 have "\<sigma> = [(v, M)]" by simp |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
444 |
with occ_elim[OF no_occ] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
445 |
show ?case by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
446 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
447 |
case (6 c d) thus ?case |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
448 |
by (cases "c = d") auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
449 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
450 |
case (7 M N M' N' \<sigma>) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
451 |
then obtain \<theta>1 \<theta>2 |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
452 |
where "unify M M' = Some \<theta>1" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
453 |
and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
454 |
and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
455 |
and ih1: "?P M M' \<theta>1" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
456 |
and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
457 |
by (auto split:option.split_asm) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
458 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
459 |
from `unify_dom (M \<cdot> N, M' \<cdot> N')` |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
460 |
have "unify_dom (M, M')" |
23777 | 461 |
by (rule accp_downward) (rule unify_rel.intros) |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
462 |
hence no_new_vars: |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
463 |
"\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t" |
23373 | 464 |
by (rule unify_vars) (rule `unify M M' = Some \<theta>1`) |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
465 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
466 |
from ih2 show ?case |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
467 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
468 |
assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
469 |
then obtain v |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
470 |
where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
471 |
and el: "elim \<theta>2 v" by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
472 |
with no_new_vars show ?thesis unfolding \<sigma> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
473 |
by (auto simp:elim_def) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
474 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
475 |
assume empty[simp]: "\<theta>2 =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
476 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
477 |
have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma> |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
478 |
by (rule compose_eqv) auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
479 |
also have "\<dots> =\<^sub>s \<theta>1" by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
480 |
finally have "\<sigma> =\<^sub>s \<theta>1" . |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
481 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
482 |
from ih1 show ?thesis |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
483 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
484 |
assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
485 |
with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
486 |
show ?thesis by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
487 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
488 |
note `\<sigma> =\<^sub>s \<theta>1` |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
489 |
also assume "\<theta>1 =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
490 |
finally show ?thesis .. |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
491 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
492 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
493 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
494 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
495 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
496 |
subsection {* Termination proof *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
497 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
498 |
termination unify |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
499 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
500 |
let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N), |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
501 |
\<lambda>(M, N). size M]" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
502 |
show "wf ?R" by simp |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
503 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
504 |
fix M N M' N' |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
505 |
show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
506 |
by (rule measures_lesseq) (auto intro: card_mono) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
507 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
508 |
fix \<theta> -- "Outer call" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
509 |
assume inner: "unify_dom (M, M')" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
510 |
"unify M M' = Some \<theta>" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
511 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
512 |
from unify_eliminates[OF inner] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
513 |
show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
514 |
proof |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
515 |
-- {* Either a variable is eliminated \ldots *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
516 |
assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
517 |
then obtain v |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
518 |
where "elim \<theta> v" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
519 |
and "v\<in>vars_of M \<union> vars_of M'" by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
520 |
with unify_vars[OF inner] |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
521 |
have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
522 |
\<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
523 |
by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
524 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
525 |
thus ?thesis |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
526 |
by (auto intro!: measures_less intro: psubset_card_mono) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
527 |
next |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
528 |
-- {* Or the substitution is empty *} |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
529 |
assume "\<theta> =\<^sub>s []" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
530 |
hence "N \<triangleleft> \<theta> = N" |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
531 |
and "N' \<triangleleft> \<theta> = N'" by auto |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
532 |
thus ?thesis |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
533 |
by (auto intro!: measures_less intro: psubset_card_mono) |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
534 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
535 |
qed |
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
diff
changeset
|
536 |
|
23219 | 537 |
end |