# HG changeset patch
# User krauss
# Date 1313957584 -7200
# Node ID 91e8062605d575b864299309cd2c9e90b1650c6c
# Parent  74c08021ab2e741643cec4e07cf69ccc6953187f
ported some lemmas from HOL/Subst/*;
tuned order

diff -r 74c08021ab2e -r 91e8062605d5 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -24,13 +24,43 @@
 *}
 
 
-subsection {* Basic definitions *}
+subsection {* Terms *}
+
+text {* Binary trees with leaves that are constants or variables. *}
 
 datatype 'a trm = 
   Var 'a 
   | Const 'a
   | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
 
+primrec vars_of :: "'a trm \<Rightarrow> 'a set"
+where
+  "vars_of (Var v) = {v}"
+| "vars_of (Const c) = {}"
+| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
+
+fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54) 
+where
+  "occs u (Var v) = False"
+| "occs u (Const c) = False"
+| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
+
+
+lemma finite_vars_of[intro]: "finite (vars_of t)"
+  by (induct t) simp_all
+
+lemma vars_var_iff: "v \<in> vars_of (Var w) \<longleftrightarrow> w = v"
+  by auto
+
+lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
+  by (induct t) auto
+
+lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
+  by (induct N) auto
+
+
+subsection {* Substitutions *}
+
 type_synonym 'a subst = "('a \<times> 'a trm) list"
 
 text {* Applying a substitution to a variable: *}
@@ -48,73 +78,77 @@
 | "(Const c) \<lhd> s = (Const c)"
 | "(M \<cdot> N) \<lhd> s = (M \<lhd> s) \<cdot> (N \<lhd> s)"
 
-text {* Composition of substitutions: *}
+definition subst_eq (infixr "\<doteq>" 52)
+where
+  "s1 \<doteq> s2 \<longleftrightarrow> (\<forall>t. t \<lhd> s1 = t \<lhd> s2)" 
 
-fun
-  comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
+fun comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
 where
   "[] \<lozenge> bl = bl"
 | "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
 
-text {* Equivalence of substitutions: *}
+
+subsection {* Basic Laws *}
+
+lemma subst_Nil[simp]: "t \<lhd> [] = t"
+by (induct t) auto
+
+lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
+by (induct u) auto
+
+lemma agreement: "(t \<lhd> r = t \<lhd> s) \<longleftrightarrow> (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
+by (induct t) auto
+
+lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
+by (simp add: agreement)
 
-definition subst_eq (infixr "\<doteq>" 52)
-where
-  "s1 \<doteq> s2 \<equiv> \<forall>t. t \<lhd> s1 = t \<lhd> s2" 
+lemma Var_in_subst:
+  "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
+by (induct t) auto
+
+lemma subst_refl[iff]: "s \<doteq> s"
+  by (auto simp:subst_eq_def)
+
+lemma subst_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
+  by (auto simp:subst_eq_def)
+
+lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
+  by (auto simp:subst_eq_def)
+
+text {* Composition of Substitutions *}
 
 
-subsection {* Basic lemmas *}
-
-lemma apply_empty[simp]: "t \<lhd> [] = t"
-by (induct t) auto
-
-lemma compose_empty[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
+lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
 by (induct \<sigma>) auto
 
-lemma apply_compose[simp]: "t \<lhd> (s1 \<lozenge> s2) = t \<lhd> s1 \<lhd> s2"
+lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
 proof (induct t)
-  case Comb thus ?case by simp
-next 
-  case Const thus ?case by simp
-next
   case (Var v) thus ?case
-  proof (induct s1)
-    case Nil show ?case by simp
-  next
-    case (Cons p s1s) thus ?case by (cases p, simp)
-  qed
-qed
+    by (induct r) auto
+qed auto
 
-lemma eqv_refl[intro]: "s \<doteq> s"
+lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
   by (auto simp:subst_eq_def)
 
-lemma eqv_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
-  by (auto simp:subst_eq_def)
-
-lemma eqv_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
-  by (auto simp:subst_eq_def)
-
-lemma eqv_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
+lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
   by (auto simp:subst_eq_def)
 
-lemma eqv_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
-  by (auto simp:subst_eq_def)
+lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
+  by auto
 
-lemma compose_eqv: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
-  by (auto simp:subst_eq_def)
+lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
+  by (auto simp: subst_eq_def)
 
-lemma compose_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
-  by auto
 
 
 subsection {* Specification: Most general unifiers *}
 
-definition
-  "Unifier \<sigma> t u \<equiv> (t\<lhd>\<sigma> = u\<lhd>\<sigma>)"
+definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
+where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
 
-definition
-  "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
-  \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
+definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
+  "MGU \<sigma> t u \<longleftrightarrow> 
+   Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
 
 lemma MGUI[intro]:
   "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
@@ -126,15 +160,13 @@
   by (auto simp:MGU_def Unifier_def)
 
 
+definition Idem :: "'a subst \<Rightarrow> bool"
+where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
+
+
+
 subsection {* The unification algorithm *}
 
-text {* Occurs check: Proper subterm relation *}
-
-fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "<:" 54) 
-where
-  "occs u (Var v) = False"
-| "occs u (Const c) = False"
-| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
 
 text {* The unification algorithm: *}
 
@@ -226,7 +258,7 @@
       by auto
 
     from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
-      by (simp add:eqv_dest[OF eqv])
+      by (simp add:subst_eq_dest[OF eqv])
 
     with MGU_outer obtain \<rho>
       where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
@@ -234,7 +266,7 @@
       by auto
     
     have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
-      by (rule eqv_intro, auto simp:eqv_dest[OF eqv] eqv_dest[OF eqv2])
+      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
     thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   qed
 qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
@@ -242,16 +274,6 @@
 
 subsection {* Properties used in termination proof *}
 
-text {* The variables of a term: *}
-
-fun vars_of:: "'a trm \<Rightarrow> 'a set"
-where
-  "vars_of (Var v) = { v }"
-| "vars_of (Const c) = {}"
-| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
-
-lemma vars_of_finite[intro]: "finite (vars_of t)"
-  by (induct t) simp_all
 
 text {* Elimination of variables by a substitution: *}
 
@@ -474,7 +496,7 @@
     assume empty[simp]: "\<theta>2 \<doteq> []"
 
     have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
-      by (rule compose_eqv) auto
+      by (rule subst_cong) auto
     also have "\<dots> \<doteq> \<theta>1" by auto
     finally have "\<sigma> \<doteq> \<theta>1" .