src/HOL/ex/Unification.thy
author krauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 44372 f9825056dbab
parent 44371 3a10392fb8c3
child 44373 7321d628b57d
permissions -rw-r--r--
more precise authors and comments;
tuned order and headers
krauss@44372
     1
(*  Title:      HOL/ex/Unification.thy
krauss@44372
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
krauss@44372
     3
    Author:     Konrad Slind, TUM & Cambridge University Computer Laboratory
krauss@44372
     4
    Author:     Alexander Krauss, TUM
krauss@22999
     5
*)
krauss@22999
     6
krauss@44372
     7
header {* Substitution and Unification *}
krauss@22999
     8
wenzelm@23219
     9
theory Unification
krauss@22999
    10
imports Main
wenzelm@23219
    11
begin
krauss@22999
    12
krauss@22999
    13
text {* 
krauss@44372
    14
  Implements Manna & Waldinger's formalization, with Paulson's
krauss@44372
    15
  simplifications, and some new simplifications by Slind and Krauss.
krauss@44372
    16
krauss@44372
    17
  Z Manna & R Waldinger, Deductive Synthesis of the Unification
krauss@44372
    18
  Algorithm.  SCP 1 (1981), 5-48
krauss@22999
    19
krauss@44372
    20
  L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
krauss@44372
    21
  (1985), 143-170
krauss@22999
    22
krauss@44372
    23
  K Slind, Reasoning about Terminating Functional Programs,
krauss@44372
    24
  Ph.D. thesis, TUM, 1999, Sect. 5.8
krauss@44372
    25
krauss@44372
    26
  A Krauss, Partial and Nested Recursive Function Definitions in
krauss@44372
    27
  Higher-Order Logic, JAR 44(4):303–336, 2010. Sect. 6.3
krauss@22999
    28
*}
krauss@22999
    29
wenzelm@23219
    30
krauss@44368
    31
subsection {* Terms *}
krauss@44368
    32
krauss@44368
    33
text {* Binary trees with leaves that are constants or variables. *}
krauss@22999
    34
krauss@22999
    35
datatype 'a trm = 
krauss@22999
    36
  Var 'a 
krauss@22999
    37
  | Const 'a
krauss@44367
    38
  | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
krauss@22999
    39
krauss@44368
    40
primrec vars_of :: "'a trm \<Rightarrow> 'a set"
krauss@44368
    41
where
krauss@44368
    42
  "vars_of (Var v) = {v}"
krauss@44368
    43
| "vars_of (Const c) = {}"
krauss@44368
    44
| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
krauss@44368
    45
krauss@44368
    46
fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54) 
krauss@44368
    47
where
krauss@44369
    48
  "u \<prec> Var v \<longleftrightarrow> False"
krauss@44369
    49
| "u \<prec> Const c \<longleftrightarrow> False"
krauss@44369
    50
| "u \<prec> M \<cdot> N \<longleftrightarrow> u = M \<or> u = N \<or> u \<prec> M \<or> u \<prec> N"
krauss@44368
    51
krauss@44368
    52
krauss@44368
    53
lemma finite_vars_of[intro]: "finite (vars_of t)"
krauss@44368
    54
  by (induct t) simp_all
krauss@44368
    55
krauss@44368
    56
lemma vars_var_iff: "v \<in> vars_of (Var w) \<longleftrightarrow> w = v"
krauss@44368
    57
  by auto
krauss@44368
    58
krauss@44368
    59
lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
krauss@44368
    60
  by (induct t) auto
krauss@44368
    61
krauss@44368
    62
lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
krauss@44368
    63
  by (induct N) auto
krauss@44368
    64
krauss@44368
    65
krauss@44368
    66
subsection {* Substitutions *}
krauss@44368
    67
wenzelm@42463
    68
type_synonym 'a subst = "('a \<times> 'a trm) list"
krauss@22999
    69
krauss@22999
    70
fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
krauss@22999
    71
where
krauss@22999
    72
  "assoc x d [] = d"
krauss@22999
    73
| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
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
lemma subst_Nil[simp]: "t \<lhd> [] = t"
krauss@44368
    91
by (induct t) auto
krauss@44368
    92
krauss@44368
    93
lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
krauss@44368
    94
by (induct u) auto
krauss@44368
    95
krauss@44368
    96
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
    97
by (induct t) auto
krauss@44368
    98
krauss@44368
    99
lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
krauss@44368
   100
by (simp add: agreement)
krauss@22999
   101
krauss@44368
   102
lemma Var_in_subst:
krauss@44368
   103
  "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
krauss@44368
   104
by (induct t) auto
krauss@44368
   105
krauss@44370
   106
lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
krauss@44370
   107
by (induct t) simp_all
krauss@44370
   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@44371
   118
lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
krauss@44371
   119
  \<Longrightarrow> t \<lhd> [(v,s)] = t"
krauss@44371
   120
by (induct t) auto
krauss@44370
   121
krauss@44368
   122
lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
krauss@22999
   123
by (induct \<sigma>) auto
krauss@22999
   124
krauss@44368
   125
lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
krauss@22999
   126
proof (induct t)
krauss@22999
   127
  case (Var v) thus ?case
krauss@44368
   128
    by (induct r) auto
krauss@44368
   129
qed auto
krauss@22999
   130
krauss@44368
   131
lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
krauss@44367
   132
  by (auto simp:subst_eq_def)
krauss@22999
   133
krauss@44368
   134
lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
krauss@44367
   135
  by (auto simp:subst_eq_def)
krauss@22999
   136
krauss@44368
   137
lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
krauss@44368
   138
  by auto
krauss@22999
   139
krauss@44368
   140
lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
krauss@44368
   141
  by (auto simp: subst_eq_def)
krauss@22999
   142
krauss@44370
   143
lemma var_self: "[(v, Var v)] \<doteq> []"
krauss@44370
   144
proof
krauss@44370
   145
  fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
krauss@44370
   146
    by (induct t) simp_all
krauss@44370
   147
qed
krauss@44370
   148
krauss@44370
   149
lemma var_same[simp]: "[(v, t)] \<doteq> [] \<longleftrightarrow> t = Var v"
krauss@44370
   150
by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
krauss@22999
   151
wenzelm@23219
   152
krauss@44372
   153
subsection {* Unifiers and Most General Unifiers *}
krauss@22999
   154
krauss@44368
   155
definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
krauss@44368
   156
where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
krauss@22999
   157
krauss@44368
   158
definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
krauss@44368
   159
  "MGU \<sigma> t u \<longleftrightarrow> 
krauss@44368
   160
   Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
krauss@22999
   161
krauss@22999
   162
lemma MGUI[intro]:
krauss@44367
   163
  "\<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
   164
  \<Longrightarrow> MGU \<sigma> t u"
krauss@22999
   165
  by (simp only:Unifier_def MGU_def, auto)
krauss@22999
   166
krauss@22999
   167
lemma MGU_sym[sym]:
krauss@22999
   168
  "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
krauss@22999
   169
  by (auto simp:MGU_def Unifier_def)
krauss@22999
   170
krauss@44371
   171
lemma MGU_is_Unifier: "MGU \<sigma> t u \<Longrightarrow> Unifier \<sigma> t u"
krauss@44371
   172
unfolding MGU_def by (rule conjunct1)
krauss@44371
   173
krauss@44370
   174
lemma MGU_Var: 
krauss@44370
   175
  assumes "\<not> Var v \<prec> t"
krauss@44370
   176
  shows "MGU [(v,t)] (Var v) t"
krauss@44370
   177
proof (intro MGUI exI)
krauss@44370
   178
  show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using assms
krauss@44370
   179
    by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
krauss@44370
   180
next
krauss@44370
   181
  fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
krauss@44370
   182
  show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
krauss@44370
   183
  proof
krauss@44370
   184
    fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
krauss@44370
   185
      by (induct s) auto
krauss@44370
   186
  qed
krauss@44370
   187
qed
krauss@44370
   188
krauss@44370
   189
lemma MGU_Const: "MGU [] (Const c) (Const d) \<longleftrightarrow> c = d"
krauss@44370
   190
  by (auto simp: MGU_def Unifier_def)
krauss@44370
   191
  
krauss@22999
   192
krauss@22999
   193
subsection {* The unification algorithm *}
krauss@22999
   194
krauss@22999
   195
function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
krauss@22999
   196
where
krauss@22999
   197
  "unify (Const c) (M \<cdot> N)   = None"
krauss@22999
   198
| "unify (M \<cdot> N)   (Const c) = None"
krauss@22999
   199
| "unify (Const c) (Var v)   = Some [(v, Const c)]"
krauss@44369
   200
| "unify (M \<cdot> N)   (Var v)   = (if Var v \<prec> M \<cdot> N 
krauss@22999
   201
                                        then None
krauss@22999
   202
                                        else Some [(v, M \<cdot> N)])"
krauss@44369
   203
| "unify (Var v)   M         = (if Var v \<prec> M
krauss@22999
   204
                                        then None
krauss@22999
   205
                                        else Some [(v, M)])"
krauss@22999
   206
| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
krauss@22999
   207
| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
krauss@22999
   208
                                    None \<Rightarrow> None |
krauss@44367
   209
                                    Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
krauss@22999
   210
                                      of None \<Rightarrow> None |
krauss@44367
   211
                                         Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
krauss@22999
   212
  by pat_completeness auto
krauss@22999
   213
krauss@22999
   214
subsection {* Properties used in termination proof *}
krauss@22999
   215
krauss@22999
   216
text {* Elimination of variables by a substitution: *}
krauss@22999
   217
krauss@22999
   218
definition
krauss@44367
   219
  "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<lhd> \<sigma>)"
krauss@22999
   220
krauss@44367
   221
lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<lhd> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
krauss@22999
   222
  by (auto simp:elim_def)
krauss@22999
   223
krauss@44367
   224
lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
krauss@22999
   225
  by (auto simp:elim_def)
krauss@22999
   226
krauss@44370
   227
lemma elim_eq: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
krauss@44367
   228
  by (auto simp:elim_def subst_eq_def)
krauss@22999
   229
krauss@44369
   230
lemma occs_elim: "\<not> Var v \<prec> t 
krauss@44367
   231
  \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
krauss@44370
   232
by (metis elim_intro remove_var var_same vars_iff_occseq)
krauss@22999
   233
krauss@22999
   234
text {* The result of a unification never introduces new variables: *}
krauss@22999
   235
krauss@44370
   236
declare unify.psimps[simp]
krauss@44370
   237
krauss@22999
   238
lemma unify_vars: 
krauss@22999
   239
  assumes "unify_dom (M, N)"
krauss@22999
   240
  assumes "unify M N = Some \<sigma>"
krauss@44367
   241
  shows "vars_of (t \<lhd> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
krauss@22999
   242
  (is "?P M N \<sigma> t")
wenzelm@24444
   243
using assms
krauss@22999
   244
proof (induct M N arbitrary:\<sigma> t)
krauss@22999
   245
  case (3 c v) 
krauss@22999
   246
  hence "\<sigma> = [(v, Const c)]" by simp
wenzelm@24444
   247
  thus ?case by (induct t) auto
krauss@22999
   248
next
krauss@22999
   249
  case (4 M N v) 
krauss@44369
   250
  hence "\<not> Var v \<prec> M \<cdot> N" by auto
wenzelm@24444
   251
  with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
wenzelm@24444
   252
  thus ?case by (induct t) auto
krauss@22999
   253
next
krauss@22999
   254
  case (5 v M)
krauss@44369
   255
  hence "\<not> Var v \<prec> M" by auto
wenzelm@24444
   256
  with 5 have "\<sigma> = [(v, M)]" by simp
wenzelm@24444
   257
  thus ?case by (induct t) auto
krauss@22999
   258
next
krauss@22999
   259
  case (7 M N M' N' \<sigma>)
krauss@22999
   260
  then obtain \<theta>1 \<theta>2 
krauss@22999
   261
    where "unify M M' = Some \<theta>1"
krauss@44367
   262
    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44367
   263
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@22999
   264
    and ih1: "\<And>t. ?P M M' \<theta>1 t"
krauss@44367
   265
    and ih2: "\<And>t. ?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2 t"
krauss@22999
   266
    by (auto split:option.split_asm)
krauss@22999
   267
krauss@22999
   268
  show ?case
krauss@22999
   269
  proof
krauss@44367
   270
    fix v assume a: "v \<in> vars_of (t \<lhd> \<sigma>)"
krauss@22999
   271
    
krauss@22999
   272
    show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
krauss@22999
   273
    proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
wenzelm@32960
   274
        \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
krauss@22999
   275
      case True
krauss@44367
   276
      with ih1 have l:"\<And>t. v \<in> vars_of (t \<lhd> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
wenzelm@32960
   277
        by auto
krauss@22999
   278
      
krauss@44367
   279
      from a and ih2[where t="t \<lhd> \<theta>1"]
krauss@44367
   280
      have "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1) 
krauss@44367
   281
        \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
wenzelm@32960
   282
        by auto
krauss@22999
   283
      hence "v \<in> vars_of t"
krauss@22999
   284
      proof
krauss@44367
   285
        assume "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
wenzelm@32960
   286
        with True show ?thesis by (auto dest:l)
krauss@22999
   287
      next
krauss@44367
   288
        assume "v \<in> vars_of (t \<lhd> \<theta>1)" 
wenzelm@32960
   289
        thus ?thesis by (rule l)
krauss@22999
   290
      qed
krauss@22999
   291
      
krauss@22999
   292
      thus ?thesis by auto
krauss@22999
   293
    qed auto
krauss@22999
   294
  qed
krauss@22999
   295
qed (auto split: split_if_asm)
krauss@22999
   296
krauss@22999
   297
krauss@22999
   298
text {* The result of a unification is either the identity
krauss@22999
   299
substitution or it eliminates a variable from one of the terms: *}
krauss@22999
   300
krauss@22999
   301
lemma unify_eliminates: 
krauss@22999
   302
  assumes "unify_dom (M, N)"
krauss@22999
   303
  assumes "unify M N = Some \<sigma>"
krauss@44367
   304
  shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> \<doteq> []"
krauss@22999
   305
  (is "?P M N \<sigma>")
wenzelm@24444
   306
using assms
krauss@22999
   307
proof (induct M N arbitrary:\<sigma>)
krauss@22999
   308
  case 1 thus ?case by simp
krauss@22999
   309
next
krauss@22999
   310
  case 2 thus ?case by simp
krauss@22999
   311
next
krauss@22999
   312
  case (3 c v)
krauss@44369
   313
  have no_occs: "\<not> Var v \<prec> Const c" by simp
wenzelm@24444
   314
  with 3 have "\<sigma> = [(v, Const c)]" by simp
krauss@44367
   315
  with occs_elim[OF no_occs]
krauss@22999
   316
  show ?case by auto
krauss@22999
   317
next
krauss@22999
   318
  case (4 M N v)
krauss@44369
   319
  hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
wenzelm@24444
   320
  with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
krauss@44367
   321
  with occs_elim[OF no_occs]
krauss@22999
   322
  show ?case by auto 
krauss@22999
   323
next
krauss@22999
   324
  case (5 v M) 
krauss@44369
   325
  hence no_occs: "\<not> Var v \<prec> M" by auto
wenzelm@24444
   326
  with 5 have "\<sigma> = [(v, M)]" by simp
krauss@44367
   327
  with occs_elim[OF no_occs]
krauss@22999
   328
  show ?case by auto 
krauss@22999
   329
next 
krauss@22999
   330
  case (6 c d) thus ?case
krauss@22999
   331
    by (cases "c = d") auto
krauss@22999
   332
next
krauss@22999
   333
  case (7 M N M' N' \<sigma>)
krauss@22999
   334
  then obtain \<theta>1 \<theta>2 
krauss@22999
   335
    where "unify M M' = Some \<theta>1"
krauss@44367
   336
    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44367
   337
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@22999
   338
    and ih1: "?P M M' \<theta>1"
krauss@44367
   339
    and ih2: "?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2"
krauss@22999
   340
    by (auto split:option.split_asm)
krauss@22999
   341
krauss@22999
   342
  from `unify_dom (M \<cdot> N, M' \<cdot> N')`
krauss@22999
   343
  have "unify_dom (M, M')"
berghofe@23777
   344
    by (rule accp_downward) (rule unify_rel.intros)
krauss@22999
   345
  hence no_new_vars: 
krauss@44367
   346
    "\<And>t. vars_of (t \<lhd> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
wenzelm@23373
   347
    by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
krauss@22999
   348
krauss@22999
   349
  from ih2 show ?case 
krauss@22999
   350
  proof 
krauss@44367
   351
    assume "\<exists>v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1). elim \<theta>2 v"
krauss@22999
   352
    then obtain v 
krauss@44367
   353
      where "v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
krauss@22999
   354
      and el: "elim \<theta>2 v" by auto
krauss@22999
   355
    with no_new_vars show ?thesis unfolding \<sigma> 
krauss@22999
   356
      by (auto simp:elim_def)
krauss@22999
   357
  next
krauss@44367
   358
    assume empty[simp]: "\<theta>2 \<doteq> []"
krauss@22999
   359
krauss@44367
   360
    have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
krauss@44368
   361
      by (rule subst_cong) auto
krauss@44367
   362
    also have "\<dots> \<doteq> \<theta>1" by auto
krauss@44367
   363
    finally have "\<sigma> \<doteq> \<theta>1" .
krauss@22999
   364
krauss@22999
   365
    from ih1 show ?thesis
krauss@22999
   366
    proof
krauss@22999
   367
      assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
krauss@44370
   368
      with elim_eq[OF `\<sigma> \<doteq> \<theta>1`]
krauss@22999
   369
      show ?thesis by auto
krauss@22999
   370
    next
krauss@44367
   371
      note `\<sigma> \<doteq> \<theta>1`
krauss@44367
   372
      also assume "\<theta>1 \<doteq> []"
krauss@22999
   373
      finally show ?thesis ..
krauss@22999
   374
    qed
krauss@22999
   375
  qed
krauss@22999
   376
qed
krauss@22999
   377
krauss@44370
   378
declare unify.psimps[simp del]
krauss@22999
   379
krauss@22999
   380
subsection {* Termination proof *}
krauss@22999
   381
krauss@22999
   382
termination unify
krauss@22999
   383
proof 
krauss@22999
   384
  let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
krauss@22999
   385
                           \<lambda>(M, N). size M]"
krauss@22999
   386
  show "wf ?R" by simp
krauss@22999
   387
krauss@44370
   388
  fix M N M' N' :: "'a trm"
krauss@22999
   389
  show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
krauss@22999
   390
    by (rule measures_lesseq) (auto intro: card_mono)
krauss@22999
   391
krauss@22999
   392
  fix \<theta>                                   -- "Outer call"
krauss@22999
   393
  assume inner: "unify_dom (M, M')"
krauss@22999
   394
    "unify M M' = Some \<theta>"
krauss@22999
   395
krauss@22999
   396
  from unify_eliminates[OF inner]
krauss@44367
   397
  show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
krauss@22999
   398
  proof
krauss@22999
   399
    -- {* Either a variable is eliminated \ldots *}
krauss@22999
   400
    assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
krauss@22999
   401
    then obtain v 
wenzelm@32960
   402
      where "elim \<theta> v" 
wenzelm@32960
   403
      and "v\<in>vars_of M \<union> vars_of M'" by auto
krauss@22999
   404
    with unify_vars[OF inner]
krauss@44367
   405
    have "vars_of (N\<lhd>\<theta>) \<union> vars_of (N'\<lhd>\<theta>)
wenzelm@32960
   406
      \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
wenzelm@32960
   407
      by auto
krauss@22999
   408
    
krauss@22999
   409
    thus ?thesis
krauss@22999
   410
      by (auto intro!: measures_less intro: psubset_card_mono)
krauss@22999
   411
  next
krauss@22999
   412
    -- {* Or the substitution is empty *}
krauss@44367
   413
    assume "\<theta> \<doteq> []"
krauss@44367
   414
    hence "N \<lhd> \<theta> = N" 
krauss@44367
   415
      and "N' \<lhd> \<theta> = N'" by auto
krauss@22999
   416
    thus ?thesis 
krauss@22999
   417
       by (auto intro!: measures_less intro: psubset_card_mono)
krauss@22999
   418
  qed
krauss@22999
   419
qed
krauss@22999
   420
krauss@44370
   421
krauss@44372
   422
subsection {* Unification returns a Most General Unifier *}
krauss@44370
   423
krauss@44370
   424
lemma unify_computes_MGU:
krauss@44370
   425
  "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
krauss@44370
   426
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
krauss@44370
   427
  case (7 M N M' N' \<sigma>) -- "The interesting case"
krauss@44370
   428
krauss@44370
   429
  then obtain \<theta>1 \<theta>2 
krauss@44370
   430
    where "unify M M' = Some \<theta>1"
krauss@44370
   431
    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44370
   432
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@44370
   433
    and MGU_inner: "MGU \<theta>1 M M'" 
krauss@44370
   434
    and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
krauss@44370
   435
    by (auto split:option.split_asm)
krauss@44370
   436
krauss@44370
   437
  show ?case
krauss@44370
   438
  proof
krauss@44370
   439
    from MGU_inner and MGU_outer
krauss@44370
   440
    have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
krauss@44370
   441
      and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
krauss@44370
   442
      unfolding MGU_def Unifier_def
krauss@44370
   443
      by auto
krauss@44370
   444
    thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
krauss@44370
   445
      by simp
krauss@44370
   446
  next
krauss@44370
   447
    fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
krauss@44370
   448
    hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
krauss@44370
   449
      and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
krauss@44370
   450
krauss@44370
   451
    with MGU_inner obtain \<delta>
krauss@44370
   452
      where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
krauss@44370
   453
      unfolding MGU_def Unifier_def
krauss@44370
   454
      by auto
krauss@44370
   455
krauss@44370
   456
    from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
krauss@44370
   457
      by (simp add:subst_eq_dest[OF eqv])
krauss@44370
   458
krauss@44370
   459
    with MGU_outer obtain \<rho>
krauss@44370
   460
      where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
krauss@44370
   461
      unfolding MGU_def Unifier_def
krauss@44370
   462
      by auto
krauss@44370
   463
    
krauss@44370
   464
    have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
krauss@44370
   465
      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
krauss@44370
   466
    thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
krauss@44370
   467
  qed
krauss@44370
   468
qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
krauss@44370
   469
krauss@44372
   470
krauss@44372
   471
subsection {* Unification returns Idempotent Substitution *}
krauss@44372
   472
krauss@44372
   473
definition Idem :: "'a subst \<Rightarrow> bool"
krauss@44372
   474
where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
krauss@44372
   475
krauss@44371
   476
lemma Idem_Nil [iff]: "Idem []"
krauss@44371
   477
  by (simp add: Idem_def)
krauss@44370
   478
krauss@44371
   479
lemma Var_Idem: 
krauss@44371
   480
  assumes "~ (Var v \<prec> t)" shows "Idem [(v,t)]"
krauss@44371
   481
  unfolding Idem_def
krauss@44371
   482
proof
krauss@44371
   483
  from assms have [simp]: "t \<lhd> [(v, t)] = t"
krauss@44371
   484
    by (metis assoc.simps(2) subst.simps(1) subst_no_occs)
krauss@44371
   485
krauss@44371
   486
  fix s show "s \<lhd> [(v, t)] \<lozenge> [(v, t)] = s \<lhd> [(v, t)]"
krauss@44371
   487
    by (induct s) auto
krauss@44371
   488
qed
krauss@44371
   489
krauss@44371
   490
lemma Unifier_Idem_subst: 
krauss@44371
   491
  "Idem(r) \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
krauss@44371
   492
    Unifier (r \<lozenge> s) (t \<lhd> r) (u \<lhd> r)"
krauss@44371
   493
by (simp add: Idem_def Unifier_def subst_eq_def)
krauss@44371
   494
krauss@44371
   495
lemma Idem_comp:
krauss@44371
   496
  "Idem r \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
krauss@44371
   497
      (!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
krauss@44371
   498
    Idem (r \<lozenge> s)"
krauss@44371
   499
  apply (frule Unifier_Idem_subst, blast) 
krauss@44371
   500
  apply (force simp add: Idem_def subst_eq_def)
krauss@44371
   501
  done
krauss@44371
   502
krauss@44371
   503
theorem unify_gives_Idem:
krauss@44371
   504
  "unify M N  = Some \<sigma> \<Longrightarrow> Idem \<sigma>"
krauss@44371
   505
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
krauss@44371
   506
  case (7 M M' N N' \<sigma>)
krauss@44371
   507
krauss@44371
   508
  then obtain \<theta>1 \<theta>2 
krauss@44371
   509
    where "unify M N = Some \<theta>1"
krauss@44371
   510
    and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44371
   511
    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@44371
   512
    and "Idem \<theta>1" 
krauss@44371
   513
    and "Idem \<theta>2"
krauss@44371
   514
    by (auto split: option.split_asm)
krauss@44371
   515
krauss@44371
   516
  from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
krauss@44371
   517
    by (rule unify_computes_MGU[THEN MGU_is_Unifier])
krauss@44371
   518
krauss@44371
   519
  with `Idem \<theta>1`
krauss@44371
   520
  show "Idem \<sigma>" unfolding \<sigma>
krauss@44371
   521
  proof (rule Idem_comp)
krauss@44371
   522
    fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
krauss@44371
   523
    with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
krauss@44371
   524
      using unify_computes_MGU MGU_def by blast
krauss@44371
   525
krauss@44371
   526
    have "\<theta>2 \<lozenge> \<sigma> \<doteq> \<theta>2 \<lozenge> (\<theta>2 \<lozenge> \<gamma>)" by (rule subst_cong) (auto simp: \<sigma>)
krauss@44371
   527
    also have "... \<doteq> (\<theta>2 \<lozenge> \<theta>2) \<lozenge> \<gamma>" by (rule comp_assoc[symmetric])
krauss@44371
   528
    also have "... \<doteq> \<theta>2 \<lozenge> \<gamma>" by (rule subst_cong) (auto simp: `Idem \<theta>2`[unfolded Idem_def])
krauss@44371
   529
    also have "... \<doteq> \<sigma>" by (rule \<sigma>[symmetric])
krauss@44371
   530
    finally show "\<theta>2 \<lozenge> \<sigma> \<doteq> \<sigma>" .
krauss@44371
   531
  qed
krauss@44371
   532
qed (auto intro!: Var_Idem split: option.splits if_splits)
krauss@39754
   533
wenzelm@23219
   534
end