tuned proofs, sledgehammering overly verbose parts
authorkrauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 4437003d91bfad83b
parent 44369 02e13192a053
child 44371 3a10392fb8c3
tuned proofs, sledgehammering overly verbose parts
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.3 @@ -106,6 +106,9 @@
     1.4    "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
     1.5  by (induct t) auto
     1.6  
     1.7 +lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
     1.8 +by (induct t) simp_all
     1.9 +
    1.10  lemma subst_refl[iff]: "s \<doteq> s"
    1.11    by (auto simp:subst_eq_def)
    1.12  
    1.13 @@ -115,9 +118,9 @@
    1.14  lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
    1.15    by (auto simp:subst_eq_def)
    1.16  
    1.17 +
    1.18  text {* Composition of Substitutions *}
    1.19  
    1.20 -
    1.21  lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
    1.22  by (induct \<sigma>) auto
    1.23  
    1.24 @@ -139,6 +142,14 @@
    1.25  lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
    1.26    by (auto simp: subst_eq_def)
    1.27  
    1.28 +lemma var_self: "[(v, Var v)] \<doteq> []"
    1.29 +proof
    1.30 +  fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
    1.31 +    by (induct t) simp_all
    1.32 +qed
    1.33 +
    1.34 +lemma var_same[simp]: "[(v, t)] \<doteq> [] \<longleftrightarrow> t = Var v"
    1.35 +by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
    1.36  
    1.37  
    1.38  subsection {* Specification: Most general unifiers *}
    1.39 @@ -159,6 +170,24 @@
    1.40    "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
    1.41    by (auto simp:MGU_def Unifier_def)
    1.42  
    1.43 +lemma MGU_Var: 
    1.44 +  assumes "\<not> Var v \<prec> t"
    1.45 +  shows "MGU [(v,t)] (Var v) t"
    1.46 +proof (intro MGUI exI)
    1.47 +  show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using assms
    1.48 +    by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
    1.49 +next
    1.50 +  fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
    1.51 +  show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
    1.52 +  proof
    1.53 +    fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
    1.54 +      by (induct s) auto
    1.55 +  qed
    1.56 +qed
    1.57 +
    1.58 +lemma MGU_Const: "MGU [] (Const c) (Const d) \<longleftrightarrow> c = d"
    1.59 +  by (auto simp: MGU_def Unifier_def)
    1.60 +  
    1.61  
    1.62  definition Idem :: "'a subst \<Rightarrow> bool"
    1.63  where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
    1.64 @@ -189,89 +218,6 @@
    1.65                                           Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
    1.66    by pat_completeness auto
    1.67  
    1.68 -declare unify.psimps[simp]
    1.69 -
    1.70 -subsection {* Partial correctness *}
    1.71 -
    1.72 -text {* Some lemmas about occs and MGU: *}
    1.73 -
    1.74 -lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
    1.75 -  \<Longrightarrow> t \<lhd> [(v,s)] = t"
    1.76 -by (induct t) auto
    1.77 -
    1.78 -lemma MGU_Var[intro]: 
    1.79 -  assumes no_occs: "\<not> Var v \<prec> t"
    1.80 -  shows "MGU [(v,t)] (Var v) t"
    1.81 -proof (intro MGUI exI)
    1.82 -  show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using no_occs
    1.83 -    by (cases "Var v = t", auto simp:subst_no_occs)
    1.84 -next
    1.85 -  fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
    1.86 -  show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
    1.87 -  proof
    1.88 -    fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
    1.89 -      by (induct s) auto
    1.90 -  qed
    1.91 -qed
    1.92 -
    1.93 -declare MGU_Var[symmetric, intro]
    1.94 -
    1.95 -lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
    1.96 -  unfolding MGU_def Unifier_def
    1.97 -  by auto
    1.98 -  
    1.99 -text {* If unification terminates, then it computes most general unifiers: *}
   1.100 -
   1.101 -lemma unify_partial_correctness:
   1.102 -  assumes "unify_dom (M, N)"
   1.103 -  assumes "unify M N = Some \<sigma>"
   1.104 -  shows "MGU \<sigma> M N"
   1.105 -using assms
   1.106 -proof (induct M N arbitrary: \<sigma>)
   1.107 -  case (7 M N M' N' \<sigma>) -- "The interesting case"
   1.108 -
   1.109 -  then obtain \<theta>1 \<theta>2 
   1.110 -    where "unify M M' = Some \<theta>1"
   1.111 -    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   1.112 -    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   1.113 -    and MGU_inner: "MGU \<theta>1 M M'" 
   1.114 -    and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   1.115 -    by (auto split:option.split_asm)
   1.116 -
   1.117 -  show ?case
   1.118 -  proof
   1.119 -    from MGU_inner and MGU_outer
   1.120 -    have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
   1.121 -      and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
   1.122 -      unfolding MGU_def Unifier_def
   1.123 -      by auto
   1.124 -    thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
   1.125 -      by simp
   1.126 -  next
   1.127 -    fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
   1.128 -    hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
   1.129 -      and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
   1.130 -
   1.131 -    with MGU_inner obtain \<delta>
   1.132 -      where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
   1.133 -      unfolding MGU_def Unifier_def
   1.134 -      by auto
   1.135 -
   1.136 -    from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
   1.137 -      by (simp add:subst_eq_dest[OF eqv])
   1.138 -
   1.139 -    with MGU_outer obtain \<rho>
   1.140 -      where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
   1.141 -      unfolding MGU_def Unifier_def
   1.142 -      by auto
   1.143 -    
   1.144 -    have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
   1.145 -      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
   1.146 -    thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   1.147 -  qed
   1.148 -qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   1.149 -
   1.150 -
   1.151  subsection {* Properties used in termination proof *}
   1.152  
   1.153  
   1.154 @@ -286,93 +232,17 @@
   1.155  lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
   1.156    by (auto simp:elim_def)
   1.157  
   1.158 -lemma elim_eqv: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   1.159 +lemma elim_eq: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   1.160    by (auto simp:elim_def subst_eq_def)
   1.161  
   1.162 -
   1.163 -text {* Replacing a variable by itself yields an identity subtitution: *}
   1.164 -
   1.165 -lemma var_self[intro]: "[(v, Var v)] \<doteq> []"
   1.166 -proof
   1.167 -  fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
   1.168 -    by (induct t) simp_all
   1.169 -qed
   1.170 -
   1.171 -lemma var_same: "([(v, t)] \<doteq> []) = (t = Var v)"
   1.172 -proof
   1.173 -  assume t_v: "t = Var v"
   1.174 -  thus "[(v, t)] \<doteq> []"
   1.175 -    by auto
   1.176 -next
   1.177 -  assume id: "[(v, t)] \<doteq> []"
   1.178 -  show "t = Var v"
   1.179 -  proof -
   1.180 -    have "t = Var v \<lhd> [(v, t)]" by simp
   1.181 -    also from id have "\<dots> = Var v \<lhd> []" ..
   1.182 -    finally show ?thesis by simp
   1.183 -  qed
   1.184 -qed
   1.185 -
   1.186 -text {* A lemma about occs and elim *}
   1.187 -
   1.188 -lemma remove_var:
   1.189 -  assumes [simp]: "v \<notin> vars_of s"
   1.190 -  shows "v \<notin> vars_of (t \<lhd> [(v, s)])"
   1.191 -  by (induct t) simp_all
   1.192 -
   1.193  lemma occs_elim: "\<not> Var v \<prec> t 
   1.194    \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
   1.195 -proof (induct t)
   1.196 -  case (Var x)
   1.197 -  show ?case
   1.198 -  proof cases
   1.199 -    assume "v = x"
   1.200 -    thus ?thesis
   1.201 -      by (simp add:var_same)
   1.202 -  next
   1.203 -    assume neq: "v \<noteq> x"
   1.204 -    have "elim [(v, Var x)] v"
   1.205 -      by (auto intro!:remove_var simp:neq)
   1.206 -    thus ?thesis ..
   1.207 -  qed
   1.208 -next
   1.209 -  case (Const c)
   1.210 -  have "elim [(v, Const c)] v"
   1.211 -    by (auto intro!:remove_var)
   1.212 -  thus ?case ..
   1.213 -next
   1.214 -  case (Comb M N)
   1.215 -  
   1.216 -  hence ih1: "elim [(v, M)] v \<or> [(v, M)] \<doteq> []"
   1.217 -    and ih2: "elim [(v, N)] v \<or> [(v, N)] \<doteq> []"
   1.218 -    and nonoccs: "Var v \<noteq> M" "Var v \<noteq> N"
   1.219 -    by auto
   1.220 -
   1.221 -  from nonoccs have "\<not> [(v,M)] \<doteq> []"
   1.222 -    by (simp add:var_same)
   1.223 -  with ih1 have "elim [(v, M)] v" by blast
   1.224 -  hence "v \<notin> vars_of (Var v \<lhd> [(v,M)])" ..
   1.225 -  hence not_in_M: "v \<notin> vars_of M" by simp
   1.226 -
   1.227 -  from nonoccs have "\<not> [(v,N)] \<doteq> []"
   1.228 -    by (simp add:var_same)
   1.229 -  with ih2 have "elim [(v, N)] v" by blast
   1.230 -  hence "v \<notin> vars_of (Var v \<lhd> [(v,N)])" ..
   1.231 -  hence not_in_N: "v \<notin> vars_of N" by simp
   1.232 -
   1.233 -  have "elim [(v, M \<cdot> N)] v"
   1.234 -  proof 
   1.235 -    fix t 
   1.236 -    show "v \<notin> vars_of (t \<lhd> [(v, M \<cdot> N)])"
   1.237 -    proof (induct t)
   1.238 -      case (Var x) thus ?case by (simp add: not_in_M not_in_N)
   1.239 -    qed auto
   1.240 -  qed
   1.241 -  thus ?case ..
   1.242 -qed
   1.243 +by (metis elim_intro remove_var var_same vars_iff_occseq)
   1.244  
   1.245  text {* The result of a unification never introduces new variables: *}
   1.246  
   1.247 +declare unify.psimps[simp]
   1.248 +
   1.249  lemma unify_vars: 
   1.250    assumes "unify_dom (M, N)"
   1.251    assumes "unify M N = Some \<sigma>"
   1.252 @@ -503,7 +373,7 @@
   1.253      from ih1 show ?thesis
   1.254      proof
   1.255        assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   1.256 -      with elim_eqv[OF `\<sigma> \<doteq> \<theta>1`]
   1.257 +      with elim_eq[OF `\<sigma> \<doteq> \<theta>1`]
   1.258        show ?thesis by auto
   1.259      next
   1.260        note `\<sigma> \<doteq> \<theta>1`
   1.261 @@ -513,6 +383,7 @@
   1.262    qed
   1.263  qed
   1.264  
   1.265 +declare unify.psimps[simp del]
   1.266  
   1.267  subsection {* Termination proof *}
   1.268  
   1.269 @@ -522,7 +393,7 @@
   1.270                             \<lambda>(M, N). size M]"
   1.271    show "wf ?R" by simp
   1.272  
   1.273 -  fix M N M' N' 
   1.274 +  fix M N M' N' :: "'a trm"
   1.275    show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
   1.276      by (rule measures_lesseq) (auto intro: card_mono)
   1.277  
   1.278 @@ -555,6 +426,56 @@
   1.279    qed
   1.280  qed
   1.281  
   1.282 -declare unify.psimps[simp del]
   1.283 +
   1.284 +subsection {* Other Properties *}
   1.285 +
   1.286 +lemma unify_computes_MGU:
   1.287 +  "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
   1.288 +using assms
   1.289 +proof (induct M N arbitrary: \<sigma> rule: unify.induct)
   1.290 +  case (7 M N M' N' \<sigma>) -- "The interesting case"
   1.291 +
   1.292 +  then obtain \<theta>1 \<theta>2 
   1.293 +    where "unify M M' = Some \<theta>1"
   1.294 +    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   1.295 +    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   1.296 +    and MGU_inner: "MGU \<theta>1 M M'" 
   1.297 +    and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   1.298 +    by (auto split:option.split_asm)
   1.299 +
   1.300 +  show ?case
   1.301 +  proof
   1.302 +    from MGU_inner and MGU_outer
   1.303 +    have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
   1.304 +      and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
   1.305 +      unfolding MGU_def Unifier_def
   1.306 +      by auto
   1.307 +    thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
   1.308 +      by simp
   1.309 +  next
   1.310 +    fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
   1.311 +    hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
   1.312 +      and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
   1.313 +
   1.314 +    with MGU_inner obtain \<delta>
   1.315 +      where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
   1.316 +      unfolding MGU_def Unifier_def
   1.317 +      by auto
   1.318 +
   1.319 +    from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
   1.320 +      by (simp add:subst_eq_dest[OF eqv])
   1.321 +
   1.322 +    with MGU_outer obtain \<rho>
   1.323 +      where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
   1.324 +      unfolding MGU_def Unifier_def
   1.325 +      by auto
   1.326 +    
   1.327 +    have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
   1.328 +      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
   1.329 +    thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   1.330 +  qed
   1.331 +qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
   1.332 +
   1.333 +
   1.334  
   1.335  end