ported some lemmas from HOL/Subst/*;
authorkrauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 4436891e8062605d5
parent 44367 74c08021ab2e
child 44369 02e13192a053
ported some lemmas from HOL/Subst/*;
tuned order
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 @@ -24,13 +24,43 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -subsection {* Basic definitions *}
     1.8 +subsection {* Terms *}
     1.9 +
    1.10 +text {* Binary trees with leaves that are constants or variables. *}
    1.11  
    1.12  datatype 'a trm = 
    1.13    Var 'a 
    1.14    | Const 'a
    1.15    | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
    1.16  
    1.17 +primrec vars_of :: "'a trm \<Rightarrow> 'a set"
    1.18 +where
    1.19 +  "vars_of (Var v) = {v}"
    1.20 +| "vars_of (Const c) = {}"
    1.21 +| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
    1.22 +
    1.23 +fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54) 
    1.24 +where
    1.25 +  "occs u (Var v) = False"
    1.26 +| "occs u (Const c) = False"
    1.27 +| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
    1.28 +
    1.29 +
    1.30 +lemma finite_vars_of[intro]: "finite (vars_of t)"
    1.31 +  by (induct t) simp_all
    1.32 +
    1.33 +lemma vars_var_iff: "v \<in> vars_of (Var w) \<longleftrightarrow> w = v"
    1.34 +  by auto
    1.35 +
    1.36 +lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
    1.37 +  by (induct t) auto
    1.38 +
    1.39 +lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
    1.40 +  by (induct N) auto
    1.41 +
    1.42 +
    1.43 +subsection {* Substitutions *}
    1.44 +
    1.45  type_synonym 'a subst = "('a \<times> 'a trm) list"
    1.46  
    1.47  text {* Applying a substitution to a variable: *}
    1.48 @@ -48,73 +78,77 @@
    1.49  | "(Const c) \<lhd> s = (Const c)"
    1.50  | "(M \<cdot> N) \<lhd> s = (M \<lhd> s) \<cdot> (N \<lhd> s)"
    1.51  
    1.52 -text {* Composition of substitutions: *}
    1.53 +definition subst_eq (infixr "\<doteq>" 52)
    1.54 +where
    1.55 +  "s1 \<doteq> s2 \<longleftrightarrow> (\<forall>t. t \<lhd> s1 = t \<lhd> s2)" 
    1.56  
    1.57 -fun
    1.58 -  comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
    1.59 +fun comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
    1.60  where
    1.61    "[] \<lozenge> bl = bl"
    1.62  | "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
    1.63  
    1.64 -text {* Equivalence of substitutions: *}
    1.65 +
    1.66 +subsection {* Basic Laws *}
    1.67 +
    1.68 +lemma subst_Nil[simp]: "t \<lhd> [] = t"
    1.69 +by (induct t) auto
    1.70 +
    1.71 +lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
    1.72 +by (induct u) auto
    1.73 +
    1.74 +lemma agreement: "(t \<lhd> r = t \<lhd> s) \<longleftrightarrow> (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
    1.75 +by (induct t) auto
    1.76 +
    1.77 +lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
    1.78 +by (simp add: agreement)
    1.79  
    1.80 -definition subst_eq (infixr "\<doteq>" 52)
    1.81 -where
    1.82 -  "s1 \<doteq> s2 \<equiv> \<forall>t. t \<lhd> s1 = t \<lhd> s2" 
    1.83 +lemma Var_in_subst:
    1.84 +  "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
    1.85 +by (induct t) auto
    1.86 +
    1.87 +lemma subst_refl[iff]: "s \<doteq> s"
    1.88 +  by (auto simp:subst_eq_def)
    1.89 +
    1.90 +lemma subst_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
    1.91 +  by (auto simp:subst_eq_def)
    1.92 +
    1.93 +lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
    1.94 +  by (auto simp:subst_eq_def)
    1.95 +
    1.96 +text {* Composition of Substitutions *}
    1.97  
    1.98  
    1.99 -subsection {* Basic lemmas *}
   1.100 -
   1.101 -lemma apply_empty[simp]: "t \<lhd> [] = t"
   1.102 -by (induct t) auto
   1.103 -
   1.104 -lemma compose_empty[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
   1.105 +lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
   1.106  by (induct \<sigma>) auto
   1.107  
   1.108 -lemma apply_compose[simp]: "t \<lhd> (s1 \<lozenge> s2) = t \<lhd> s1 \<lhd> s2"
   1.109 +lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
   1.110  proof (induct t)
   1.111 -  case Comb thus ?case by simp
   1.112 -next 
   1.113 -  case Const thus ?case by simp
   1.114 -next
   1.115    case (Var v) thus ?case
   1.116 -  proof (induct s1)
   1.117 -    case Nil show ?case by simp
   1.118 -  next
   1.119 -    case (Cons p s1s) thus ?case by (cases p, simp)
   1.120 -  qed
   1.121 -qed
   1.122 +    by (induct r) auto
   1.123 +qed auto
   1.124  
   1.125 -lemma eqv_refl[intro]: "s \<doteq> s"
   1.126 +lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
   1.127    by (auto simp:subst_eq_def)
   1.128  
   1.129 -lemma eqv_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
   1.130 -  by (auto simp:subst_eq_def)
   1.131 -
   1.132 -lemma eqv_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
   1.133 -  by (auto simp:subst_eq_def)
   1.134 -
   1.135 -lemma eqv_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
   1.136 +lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
   1.137    by (auto simp:subst_eq_def)
   1.138  
   1.139 -lemma eqv_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
   1.140 -  by (auto simp:subst_eq_def)
   1.141 +lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
   1.142 +  by auto
   1.143  
   1.144 -lemma compose_eqv: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
   1.145 -  by (auto simp:subst_eq_def)
   1.146 +lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
   1.147 +  by (auto simp: subst_eq_def)
   1.148  
   1.149 -lemma compose_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
   1.150 -  by auto
   1.151  
   1.152  
   1.153  subsection {* Specification: Most general unifiers *}
   1.154  
   1.155 -definition
   1.156 -  "Unifier \<sigma> t u \<equiv> (t\<lhd>\<sigma> = u\<lhd>\<sigma>)"
   1.157 +definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   1.158 +where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
   1.159  
   1.160 -definition
   1.161 -  "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
   1.162 -  \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
   1.163 +definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
   1.164 +  "MGU \<sigma> t u \<longleftrightarrow> 
   1.165 +   Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
   1.166  
   1.167  lemma MGUI[intro]:
   1.168    "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
   1.169 @@ -126,15 +160,13 @@
   1.170    by (auto simp:MGU_def Unifier_def)
   1.171  
   1.172  
   1.173 +definition Idem :: "'a subst \<Rightarrow> bool"
   1.174 +where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
   1.175 +
   1.176 +
   1.177 +
   1.178  subsection {* The unification algorithm *}
   1.179  
   1.180 -text {* Occurs check: Proper subterm relation *}
   1.181 -
   1.182 -fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "<:" 54) 
   1.183 -where
   1.184 -  "occs u (Var v) = False"
   1.185 -| "occs u (Const c) = False"
   1.186 -| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
   1.187  
   1.188  text {* The unification algorithm: *}
   1.189  
   1.190 @@ -226,7 +258,7 @@
   1.191        by auto
   1.192  
   1.193      from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
   1.194 -      by (simp add:eqv_dest[OF eqv])
   1.195 +      by (simp add:subst_eq_dest[OF eqv])
   1.196  
   1.197      with MGU_outer obtain \<rho>
   1.198        where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
   1.199 @@ -234,7 +266,7 @@
   1.200        by auto
   1.201      
   1.202      have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
   1.203 -      by (rule eqv_intro, auto simp:eqv_dest[OF eqv] eqv_dest[OF eqv2])
   1.204 +      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
   1.205      thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   1.206    qed
   1.207  qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   1.208 @@ -242,16 +274,6 @@
   1.209  
   1.210  subsection {* Properties used in termination proof *}
   1.211  
   1.212 -text {* The variables of a term: *}
   1.213 -
   1.214 -fun vars_of:: "'a trm \<Rightarrow> 'a set"
   1.215 -where
   1.216 -  "vars_of (Var v) = { v }"
   1.217 -| "vars_of (Const c) = {}"
   1.218 -| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
   1.219 -
   1.220 -lemma vars_of_finite[intro]: "finite (vars_of t)"
   1.221 -  by (induct t) simp_all
   1.222  
   1.223  text {* Elimination of variables by a substitution: *}
   1.224  
   1.225 @@ -474,7 +496,7 @@
   1.226      assume empty[simp]: "\<theta>2 \<doteq> []"
   1.227  
   1.228      have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
   1.229 -      by (rule compose_eqv) auto
   1.230 +      by (rule subst_cong) auto
   1.231      also have "\<dots> \<doteq> \<theta>1" by auto
   1.232      finally have "\<sigma> \<doteq> \<theta>1" .
   1.233