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