src/HOL/ex/Unification.thy
author krauss
Tue Sep 28 09:54:07 2010 +0200 (2010-09-28)
changeset 39754 150f831ce4a3
parent 32960 69916a850301
child 41460 ea56b98aee83
permissions -rw-r--r--
no longer declare .psimps rules as [simp].

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