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