1.1 --- a/src/HOL/IsaMakefile	Sun Aug 21 22:13:04 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sun Aug 21 22:13:04 2011 +0200
     1.3 @@ -70,7 +70,6 @@
     1.4    HOL-SPARK-Examples \
     1.5    HOL-Word-SMT_Examples \
     1.6    HOL-Statespace \
     1.7 -  HOL-Subst \
     1.8        TLA-Buffer \
     1.9        TLA-Inc \
    1.10        TLA-Memory \
    1.11 @@ -496,15 +495,6 @@
    1.12  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
    1.13  
    1.14  
    1.15 -## HOL-Subst
    1.16 -
    1.17 -HOL-Subst: HOL $(LOG)/HOL-Subst.gz
    1.18 -
    1.19 -$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML		\
    1.20 -  Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
    1.21 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
    1.22 -
    1.23 -
    1.24  ## HOL-Induct
    1.25  
    1.26  HOL-Induct: HOL $(LOG)/HOL-Induct.gz
    1.27 @@ -1754,7 +1744,7 @@
    1.28  		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
    1.29  		$(LOG)/HOL-Word-SMT_Examples.gz				\
    1.30  		$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz	\
    1.31 -		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
    1.32 +		$(LOG)/HOL-Statespace.gz				\
    1.33  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
    1.34  		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
    1.35  		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\

     2.1 --- a/src/HOL/Subst/AList.thy	Sun Aug 21 22:13:04 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,28 +0,0 @@
     2.4 -(*  Title:      HOL/Subst/AList.thy
     2.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     2.6 -    Copyright   1993  University of Cambridge
     2.7 -*)
     2.8 -
     2.9 -header {* Association Lists *}
    2.10 -
    2.11 -theory AList
    2.12 -imports Main
    2.13 -begin
    2.14 -
    2.15 -primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    2.16 -where
    2.17 -  "alist_rec [] c d = c"
    2.18 -| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
    2.19 -
    2.20 -primrec assoc :: "['a,'b,('a*'b) list] => 'b"
    2.21 -where
    2.22 -  "assoc v d [] = d"
    2.23 -| "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    2.24 -
    2.25 -lemma alist_induct:
    2.26 -    "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
    2.27 -  by (induct l) auto
    2.28 -
    2.29 -
    2.30 -
    2.31 -end

     3.1 --- a/src/HOL/Subst/ROOT.ML	Sun Aug 21 22:13:04 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,26 +0,0 @@
     3.4 -(*  Title:      HOL/Subst/ROOT.ML
     3.5 -    Authors:    Martin Coen, Cambridge University Computer Laboratory
     3.6 -                Konrad Slind, TU Munich
     3.7 -    Copyright   1993  University of Cambridge,
     3.8 -                1996  TU Munich
     3.9 -
    3.10 -Substitution and Unification in Higher-Order Logic. 
    3.11 -
    3.12 -Implements Manna & Waldinger's formalization, with Paulson's simplifications,
    3.13 -and some new simplifications by Slind.
    3.14 -
    3.15 -Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. 
    3.16 -SCP 1 (1981), 5-48
    3.17 -
    3.18 -L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
    3.19 -
    3.20 -AList        -  association lists
    3.21 -UTerm        -  data type of terms
    3.22 -Subst        -  substitutions
    3.23 -Unifier      -  specification of unification and conditions for 
    3.24 -                correctness and termination
    3.25 -Unify        -  the unification function
    3.26 -
    3.27 -*)
    3.28 -
    3.29 -use_thys ["Unify"];

     4.1 --- a/src/HOL/Subst/Subst.thy	Sun Aug 21 22:13:04 2011 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,196 +0,0 @@
     4.4 -(*  Title:      HOL/Subst/Subst.thy
     4.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     4.6 -    Copyright   1993  University of Cambridge
     4.7 -*)
     4.8 -
     4.9 -header {* Substitutions on uterms *}
    4.10 -
    4.11 -theory Subst
    4.12 -imports AList UTerm
    4.13 -begin
    4.14 -
    4.15 -primrec
    4.16 -  subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm"  (infixl "<|" 55)
    4.17 -where
    4.18 -  subst_Var: "(Var v <| s) = assoc v (Var v) s"
    4.19 -| subst_Const: "(Const c <| s) = Const c"
    4.20 -| subst_Comb: "(Comb M N <| s) = Comb (M <| s) (N <| s)"
    4.21 -
    4.22 -notation (xsymbols)
    4.23 -  subst  (infixl "\<lhd>" 55)
    4.24 -
    4.25 -definition
    4.26 -  subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"  (infixr "=$=" 52)
    4.27 -  where "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
    4.28 -
    4.29 -notation (xsymbols)
    4.30 -  subst_eq  (infixr "\<doteq>" 52)
    4.31 -
    4.32 -definition
    4.33 -  comp :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> ('a* 'a uterm) list"
    4.34 -    (infixl "<>" 56)
    4.35 -  where "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl) # g)"
    4.36 -
    4.37 -notation (xsymbols)
    4.38 -  comp  (infixl "\<lozenge>" 56)
    4.39 -
    4.40 -definition
    4.41 -  sdom :: "('a*('a uterm)) list => 'a set" where
    4.42 -  "sdom al = alist_rec al {} (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
    4.43 -
    4.44 -definition
    4.45 -  srange :: "('a*('a uterm)) list => 'a set" where
    4.46 -  "srange al = Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})"
    4.47 -
    4.48 -
    4.49 -
    4.50 -subsection {* Basic Laws *}
    4.51 -
    4.52 -lemma subst_Nil [simp]: "t \<lhd> [] = t"
    4.53 -  by (induct t) auto
    4.54 -
    4.55 -lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
    4.56 -  by (induct u) auto
    4.57 -
    4.58 -lemma Var_not_occs: "~ (Var(v) \<prec> t) \<Longrightarrow> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s"
    4.59 -  apply (case_tac "t = Var v")
    4.60 -   prefer 2
    4.61 -   apply (erule rev_mp)+
    4.62 -   apply (rule_tac P = "%x. x \<noteq> Var v \<longrightarrow> ~(Var v \<prec> x) \<longrightarrow> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s" 
    4.63 -     in uterm.induct)
    4.64 -     apply auto
    4.65 -  done
    4.66 -
    4.67 -lemma agreement: "(t\<lhd>r = t\<lhd>s) = (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
    4.68 -  by (induct t) auto
    4.69 -
    4.70 -lemma repl_invariance: "~ v: vars_of t ==> t \<lhd> (v,u)#s = t \<lhd> s"
    4.71 -  by (simp add: agreement)
    4.72 -
    4.73 -lemma Var_in_subst:
    4.74 -    "v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)"
    4.75 -  by (induct t) auto
    4.76 -
    4.77 -
    4.78 -subsection{*Equality between Substitutions*}
    4.79 -
    4.80 -lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)"
    4.81 -  by (simp add: subst_eq_def)
    4.82 -
    4.83 -lemma subst_refl [iff]: "r \<doteq> r"
    4.84 -  by (simp add: subst_eq_iff)
    4.85 -
    4.86 -lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
    4.87 -  by (simp add: subst_eq_iff)
    4.88 -
    4.89 -lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
    4.90 -  by (simp add: subst_eq_iff)
    4.91 -
    4.92 -lemma subst_subst2:
    4.93 -    "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
    4.94 -  by (simp add: subst_eq_def)
    4.95 -
    4.96 -lemma ssubst_subst2:
    4.97 -    "[| s \<doteq> r; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
    4.98 -  by (simp add: subst_eq_def)
    4.99 -
   4.100 -
   4.101 -subsection{*Composition of Substitutions*}
   4.102 -
   4.103 -lemma [simp]: 
   4.104 -     "[] \<lozenge> bl = bl"
   4.105 -     "((a,b)#al) \<lozenge> bl = (a,b \<lhd> bl) # (al \<lozenge> bl)"
   4.106 -     "sdom([]) = {}"
   4.107 -     "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"
   4.108 -  by (simp_all add: comp_def sdom_def) 
   4.109 -
   4.110 -lemma comp_Nil [simp]: "s \<lozenge> [] = s"
   4.111 -  by (induct s) auto
   4.112 -
   4.113 -lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []"
   4.114 -  by simp
   4.115 -
   4.116 -lemma subst_comp [simp]: "(t \<lhd> r \<lozenge> s) = (t \<lhd> r \<lhd> s)"
   4.117 -  apply (induct t)
   4.118 -  apply simp_all
   4.119 -  apply (induct r)
   4.120 -   apply auto
   4.121 -  done
   4.122 -
   4.123 -lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)"
   4.124 -  by (simp add: subst_eq_iff)
   4.125 -
   4.126 -lemma subst_cong:
   4.127 -  "[| theta \<doteq> theta1; sigma \<doteq> sigma1|] 
   4.128 -    ==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)"
   4.129 -  by (simp add: subst_eq_def)
   4.130 -
   4.131 -
   4.132 -lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s"
   4.133 -  apply (simp add: subst_eq_iff)
   4.134 -  apply (rule allI)
   4.135 -  apply (induct_tac t)
   4.136 -    apply simp_all
   4.137 -  done
   4.138 -
   4.139 -
   4.140 -lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==>  t \<lhd> q \<lhd> r = t \<lhd> s"
   4.141 -  by (simp add: subst_eq_iff)
   4.142 -
   4.143 -
   4.144 -subsection{*Domain and range of Substitutions*}
   4.145 -
   4.146 -lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
   4.147 -  apply (induct s)
   4.148 -   apply (case_tac [2] a)
   4.149 -   apply auto
   4.150 -  done
   4.151 -
   4.152 -
   4.153 -lemma srange_iff: 
   4.154 -    "v \<in> srange(s) = (\<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s))"
   4.155 -  by (auto simp add: srange_def)
   4.156 -
   4.157 -lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
   4.158 -  unfolding empty_def by blast
   4.159 -
   4.160 -lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})"
   4.161 -  apply (induct t)
   4.162 -    apply (auto simp add: empty_iff_all_not sdom_iff)
   4.163 -  done
   4.164 -
   4.165 -lemma Var_in_srange:
   4.166 -    "v \<in> sdom(s) \<Longrightarrow>  v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s)"
   4.167 -  apply (induct t)
   4.168 -    apply (case_tac "a \<in> sdom s")
   4.169 -  apply (auto simp add: sdom_iff srange_iff)
   4.170 -  done
   4.171 -
   4.172 -lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==>  v \<notin> vars_of(t \<lhd> s)"
   4.173 -  by (blast intro: Var_in_srange)
   4.174 -
   4.175 -lemma Var_intro:
   4.176 -    "v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s) | v \<in> vars_of(t)"
   4.177 -  apply (induct t)
   4.178 -    apply (auto simp add: sdom_iff srange_iff)
   4.179 -  apply (rule_tac x=a in exI)
   4.180 -  apply auto 
   4.181 -  done
   4.182 -
   4.183 -lemma srangeD: "v \<in> srange(s) ==> \<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s)"
   4.184 -  by (simp add: srange_iff)
   4.185 -
   4.186 -lemma dom_range_disjoint:
   4.187 -    "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t \<lhd> s) = {})"
   4.188 -  apply (simp add: empty_iff_all_not)
   4.189 -  apply (force intro: Var_in_srange dest: srangeD)
   4.190 -  done
   4.191 -
   4.192 -lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))"
   4.193 -  by (auto simp add: empty_iff_all_not invariance)
   4.194 -
   4.195 -
   4.196 -lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
   4.197 -  by (induct M) auto
   4.198 -
   4.199 -end

     5.1 --- a/src/HOL/Subst/UTerm.thy	Sun Aug 21 22:13:04 2011 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,60 +0,0 @@
     5.4 -(*  Title:      HOL/Subst/UTerm.thy
     5.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     5.6 -    Copyright   1993  University of Cambridge
     5.7 -*)
     5.8 -
     5.9 -header {* Simple Term Structure for Unification *}
    5.10 -
    5.11 -theory UTerm
    5.12 -imports Main
    5.13 -begin
    5.14 -
    5.15 -text {* Binary trees with leaves that are constants or variables. *}
    5.16 -
    5.17 -datatype 'a uterm =
    5.18 -    Var 'a
    5.19 -  | Const 'a
    5.20 -  | Comb "'a uterm" "'a uterm"
    5.21 -
    5.22 -primrec vars_of :: "'a uterm => 'a set"
    5.23 -where
    5.24 -  vars_of_Var:   "vars_of (Var v) = {v}"
    5.25 -| vars_of_Const: "vars_of (Const c) = {}"
    5.26 -| vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
    5.27 -
    5.28 -primrec occs :: "'a uterm => 'a uterm => bool"   (infixl "<:" 54) 
    5.29 -where
    5.30 -  occs_Var: "u <: (Var v) = False"
    5.31 -| occs_Const: "u <: (Const c) = False"
    5.32 -| occs_Comb: "u <: (Comb M N) = (u = M | u = N | u <: M | u <: N)"
    5.33 -
    5.34 -notation (xsymbols)
    5.35 -  occs  (infixl "\<prec>" 54)
    5.36 -
    5.37 -primrec uterm_size ::  "'a uterm => nat"
    5.38 -where
    5.39 -  uterm_size_Var: "uterm_size (Var v) = 0"
    5.40 -| uterm_size_Const: "uterm_size (Const c) = 0"
    5.41 -| uterm_size_Comb: "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
    5.42 -
    5.43 -
    5.44 -lemma vars_var_iff: "(v \<in> vars_of (Var w)) = (w = v)"
    5.45 -  by auto
    5.46 -
    5.47 -lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)"
    5.48 -  by (induct t) auto
    5.49 -
    5.50 -
    5.51 -text{* Not used, but perhaps useful in other proofs *}
    5.52 -lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
    5.53 -  by (induct N) auto
    5.54 -
    5.55 -
    5.56 -lemma monotone_vars_of:
    5.57 -    "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
    5.58 -  by blast
    5.59 -
    5.60 -lemma finite_vars_of: "finite (vars_of M)"
    5.61 -  by (induct M) auto
    5.62 -
    5.63 -end

     6.1 --- a/src/HOL/Subst/Unifier.thy	Sun Aug 21 22:13:04 2011 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,91 +0,0 @@
     6.4 -(*  Title:      HOL/Subst/Unifier.thy
     6.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     6.6 -    Copyright   1993  University of Cambridge
     6.7 -
     6.8 -*)
     6.9 -
    6.10 -header {* Definition of Most General Unifier *}
    6.11 -
    6.12 -theory Unifier
    6.13 -imports Subst
    6.14 -begin
    6.15 -
    6.16 -definition
    6.17 -  Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
    6.18 -  where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
    6.19 -
    6.20 -definition
    6.21 -  MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool"  (infixr ">>" 52)
    6.22 -  where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
    6.23 -
    6.24 -definition
    6.25 -  MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
    6.26 -  where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
    6.27 -
    6.28 -definition
    6.29 -  Idem :: "('a * 'a uterm)list => bool" where
    6.30 -  "Idem s \<longleftrightarrow> (s <> s) =$= s"
    6.31 -
    6.32 -
    6.33 -lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
    6.34 -
    6.35 -
    6.36 -subsection {* Unifiers *}
    6.37 -
    6.38 -lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
    6.39 -  by (simp add: Unifier_def)
    6.40 -
    6.41 -
    6.42 -lemma Cons_Unifier: "v \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> Unifier ((v, r) #s) t u"
    6.43 -  by (simp add: Unifier_def repl_invariance)
    6.44 -
    6.45 -
    6.46 -subsection {* Most General Unifiers *}
    6.47 -
    6.48 -lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
    6.49 -  by (simp add: unify_defs eq_commute)
    6.50 -
    6.51 -
    6.52 -lemma MoreGen_Nil [iff]: "[] >> s"
    6.53 -  by (auto simp add: MoreGeneral_def)
    6.54 -
    6.55 -lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"
    6.56 -  apply (unfold unify_defs)
    6.57 -  apply (auto intro: ssubst_subst2 subst_comp_Nil)
    6.58 -  done
    6.59 -
    6.60 -lemma MGUnifier_Var [intro!]: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
    6.61 -  apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
    6.62 -  apply safe
    6.63 -   apply (rule exI)
    6.64 -   apply (erule subst, rule Cons_trivial [THEN subst_sym])
    6.65 -  apply (erule ssubst_subst2)
    6.66 -  apply (simp (no_asm_simp) add: Var_not_occs)
    6.67 -  done
    6.68 -
    6.69 -
    6.70 -subsection {* Idempotence *}
    6.71 -
    6.72 -lemma Idem_Nil [iff]: "Idem []"
    6.73 -  by (simp add: Idem_def)
    6.74 -
    6.75 -lemma Idem_iff: "Idem s = (sdom s Int srange s = {})"
    6.76 -  by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
    6.77 -
    6.78 -lemma Var_Idem [intro!]: "~ (Var v <: t) ==> Idem [(v,t)]"
    6.79 -  by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
    6.80 -
    6.81 -lemma Unifier_Idem_subst: 
    6.82 -  "Idem(r) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
    6.83 -    Unifier (r <> s) (t <| r) (u <| r)"
    6.84 -  by (simp add: Idem_def Unifier_def comp_subst_subst)
    6.85 -
    6.86 -lemma Idem_comp:
    6.87 -  "Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
    6.88 -      (!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
    6.89 -    Idem (r <> s)"
    6.90 -  apply (frule Unifier_Idem_subst, blast) 
    6.91 -  apply (force simp add: Idem_def subst_eq_iff)
    6.92 -  done
    6.93 -
    6.94 -end

     7.1 --- a/src/HOL/Subst/Unify.thy	Sun Aug 21 22:13:04 2011 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,235 +0,0 @@
     7.4 -(*  Title:      HOL/Subst/Unify.thy
     7.5 -    Author:     Konrad Slind, Cambridge University Computer Laboratory
     7.6 -    Copyright   1997  University of Cambridge
     7.7 -*)
     7.8 -
     7.9 -header {* Unification Algorithm *}
    7.10 -
    7.11 -theory Unify
    7.12 -imports Unifier "~~/src/HOL/Library/Old_Recdef"
    7.13 -begin
    7.14 -
    7.15 -subsection {* Substitution and Unification in Higher-Order Logic. *}
    7.16 -
    7.17 -text {*
    7.18 -NB: This theory is already quite old.
    7.19 -You might want to look at the newer Isar formalization of
    7.20 -unification in HOL/ex/Unification.thy.
    7.21 -
    7.22 -Implements Manna and Waldinger's formalization, with Paulson's simplifications,
    7.23 -and some new simplifications by Slind.
    7.24 -
    7.25 -Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm.
    7.26 -SCP 1 (1981), 5-48
    7.27 -
    7.28 -L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
    7.29 -*}
    7.30 -
    7.31 -definition
    7.32 -  unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
    7.33 -  "unifyRel = inv_image (finite_psubset <*lex*> measure uterm_size)
    7.34 -      (%(M,N). (vars_of M Un vars_of N, M))"
    7.35 -   --{*Termination relation for the Unify function:
    7.36 -         either the set of variables decreases,
    7.37 -         or the first argument does (in fact, both do) *}
    7.38 -
    7.39 -
    7.40 -text{* Wellfoundedness of unifyRel *}
    7.41 -lemma wf_unifyRel [iff]: "wf unifyRel"
    7.42 -  by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
    7.43 -
    7.44 -consts unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
    7.45 -recdef (permissive) unify "unifyRel"
    7.46 - unify_CC: "unify(Const m, Const n)  = (if (m=n) then Some[] else None)"
    7.47 - unify_CB: "unify(Const m, Comb M N) = None"
    7.48 - unify_CV: "unify(Const m, Var v)    = Some[(v,Const m)]"
    7.49 - unify_V:  "unify(Var v, M) = (if (Var v \<prec> M) then None else Some[(v,M)])"
    7.50 - unify_BC: "unify(Comb M N, Const x) = None"
    7.51 - unify_BV: "unify(Comb M N, Var v)   = (if (Var v \<prec> Comb M N) then None
    7.52 -                                        else Some[(v,Comb M N)])"
    7.53 - unify_BB:
    7.54 -  "unify(Comb M1 N1, Comb M2 N2) =
    7.55 -      (case unify(M1,M2)
    7.56 -        of None       => None
    7.57 -         | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta)
    7.58 -                            of None       => None
    7.59 -                             | Some sigma => Some (theta \<lozenge> sigma)))"
    7.60 -  (hints recdef_wf: wf_unifyRel)
    7.61 -
    7.62 -
    7.63 -text{* This file defines a nested unification algorithm, then proves that it
    7.64 - terminates, then proves 2 correctness theorems: that when the algorithm
    7.65 - succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
    7.66 - Although the proofs may seem long, they are actually quite direct, in that
    7.67 - the correctness and termination properties are not mingled as much as in
    7.68 - previous proofs of this algorithm.*}
    7.69 -
    7.70 -(*---------------------------------------------------------------------------
    7.71 - * Our approach for nested recursive functions is as follows:
    7.72 - *
    7.73 - *    0. Prove the wellfoundedness of the termination relation.
    7.74 - *    1. Prove the non-nested termination conditions.
    7.75 - *    2. Eliminate (0) and (1) from the recursion equations and the
    7.76 - *       induction theorem.
    7.77 - *    3. Prove the nested termination conditions by using the induction
    7.78 - *       theorem from (2) and by using the recursion equations from (2).
    7.79 - *       These are constrained by the nested termination conditions, but
    7.80 - *       things work out magically (by wellfoundedness of the termination
    7.81 - *       relation).
    7.82 - *    4. Eliminate the nested TCs from the results of (2).
    7.83 - *    5. Prove further correctness properties using the results of (4).
    7.84 - *
    7.85 - * Deeper nestings require iteration of steps (3) and (4).
    7.86 - *---------------------------------------------------------------------------*)
    7.87 -
    7.88 -text{*The non-nested TC (terminiation condition).*}
    7.89 -recdef_tc unify_tc1: unify (1)
    7.90 -  by (auto simp: unifyRel_def finite_psubset_def finite_vars_of)
    7.91 -
    7.92 -
    7.93 -text{*Termination proof.*}
    7.94 -
    7.95 -lemma trans_unifyRel: "trans unifyRel"
    7.96 -  by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
    7.97 -    trans_finite_psubset)
    7.98 -
    7.99 -
   7.100 -text{*The following lemma is used in the last step of the termination proof
   7.101 -for the nested call in Unify.  Loosely, it says that unifyRel doesn't care
   7.102 -about term structure.*}
   7.103 -lemma Rassoc:
   7.104 -  "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel  ==>
   7.105 -    ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
   7.106 -  by (simp add: less_eq add_assoc Un_assoc unifyRel_def lex_prod_def)
   7.107 -
   7.108 -
   7.109 -text{*This lemma proves the nested termination condition for the base cases
   7.110 - * 3, 4, and 6.*}
   7.111 -lemma var_elimR:
   7.112 -  "~(Var x \<prec> M) ==>
   7.113 -    ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel
   7.114 -  & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel"
   7.115 -apply (case_tac "Var x = M", clarify, simp)
   7.116 -apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
   7.117 -txt{*@{text uterm_less} case*}
   7.118 -apply (simp add: less_eq unifyRel_def lex_prod_def)
   7.119 -apply blast
   7.120 -txt{*@{text finite_psubset} case*}
   7.121 -apply (simp add: unifyRel_def lex_prod_def)
   7.122 -apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
   7.123 -apply blast
   7.124 -txt{*Final case, also @{text finite_psubset}*}
   7.125 -apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
   7.126 -apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim)
   7.127 -apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim)
   7.128 -apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
   7.129 -apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff)
   7.130 -done
   7.131 -
   7.132 -
   7.133 -text{*Eliminate tc1 from the recursion equations and the induction theorem.*}
   7.134 -
   7.135 -lemmas unify_nonrec [simp] =
   7.136 -       unify_CC unify_CB unify_CV unify_V unify_BC unify_BV
   7.137 -
   7.138 -lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1]
   7.139 -
   7.140 -lemmas unify_induct0 = unify.induct [OF unify_tc1]
   7.141 -
   7.142 -text{*The nested TC. The (2) requests the second one.
   7.143 -      Proved by recursion induction.*}
   7.144 -recdef_tc unify_tc2: unify (2)
   7.145 -txt{*The extracted TC needs the scope of its quantifiers adjusted, so our
   7.146 - first step is to restrict the scopes of N1 and N2.*}
   7.147 -apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta -->
   7.148 -      (\<forall>N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> unifyRel)")
   7.149 -apply blast
   7.150 -apply (rule allI)
   7.151 -apply (rule allI)
   7.152 -txt{*Apply induction on this still-quantified formula*}
   7.153 -apply (rule_tac u = M1 and v = M2 in unify_induct0)
   7.154 -      apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
   7.155 - txt{*Const-Const case*}
   7.156 - apply (simp add: unifyRel_def lex_prod_def less_eq)
   7.157 -txt{*Comb-Comb case*}
   7.158 -apply (simp (no_asm_simp) split add: option.split)
   7.159 -apply (intro strip)
   7.160 -apply (rule trans_unifyRel [THEN transD], blast)
   7.161 -apply (simp only: subst_Comb [symmetric])
   7.162 -apply (rule Rassoc, blast)
   7.163 -done
   7.164 -
   7.165 -
   7.166 -text{* Now for elimination of nested TC from unify.simps and induction.*}
   7.167 -
   7.168 -text{*Desired rule, copied from the theory file.*}
   7.169 -lemma unifyCombComb [simp]:
   7.170 -    "unify(Comb M1 N1, Comb M2 N2) =
   7.171 -       (case unify(M1,M2)
   7.172 -         of None => None
   7.173 -          | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta)
   7.174 -                             of None => None
   7.175 -                              | Some sigma => Some (theta \<lozenge> sigma)))"
   7.176 -by (simp add: unify_tc2 unify_simps0 split add: option.split)
   7.177 -
   7.178 -lemma unify_induct:
   7.179 -  "(\<And>m n. P (Const m) (Const n)) \<Longrightarrow>
   7.180 -  (\<And>m M N. P (Const m) (Comb M N)) \<Longrightarrow>
   7.181 -  (\<And>m v. P (Const m) (Var v)) \<Longrightarrow>
   7.182 -  (\<And>v M. P (Var v) M) \<Longrightarrow>
   7.183 -  (\<And>M N x. P (Comb M N) (Const x)) \<Longrightarrow>
   7.184 -  (\<And>M N v. P (Comb M N) (Var v)) \<Longrightarrow>
   7.185 -  (\<And>M1 N1 M2 N2.
   7.186 -    \<forall>theta. unify (M1, M2) = Some theta \<longrightarrow> P (N1 \<lhd> theta) (N2 \<lhd> theta) \<Longrightarrow>
   7.187 -    P M1 M2 \<Longrightarrow> P (Comb M1 N1) (Comb M2 N2)) \<Longrightarrow>
   7.188 -  P u v"
   7.189 -by (rule unify_induct0) (simp_all add: unify_tc2)
   7.190 -
   7.191 -text{*Correctness. Notice that idempotence is not needed to prove that the
   7.192 -algorithm terminates and is not needed to prove the algorithm correct, if you
   7.193 -are only interested in an MGU.  This is in contrast to the approach of M&W,
   7.194 -who used idempotence and MGU-ness in the termination proof.*}
   7.195 -
   7.196 -theorem unify_gives_MGU [rule_format]:
   7.197 -     "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N"
   7.198 -apply (rule_tac u = M and v = N in unify_induct0)
   7.199 -    apply (simp_all (no_asm_simp))
   7.200 -    txt{*Const-Const case*}
   7.201 -    apply (simp add: MGUnifier_def Unifier_def)
   7.202 -   txt{*Const-Var case*}
   7.203 -   apply (subst mgu_sym)
   7.204 -   apply (simp add: MGUnifier_Var)
   7.205 -  txt{*Var-M case*}
   7.206 -  apply (simp add: MGUnifier_Var)
   7.207 - txt{*Comb-Var case*}
   7.208 - apply (subst mgu_sym)
   7.209 - apply (simp add: MGUnifier_Var)
   7.210 -txt{*Comb-Comb case*}
   7.211 -apply (simp add: unify_tc2)
   7.212 -apply (simp (no_asm_simp) split add: option.split)
   7.213 -apply (intro strip)
   7.214 -apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def)
   7.215 -apply (safe, rename_tac theta sigma gamma)
   7.216 -apply (erule_tac x = gamma in allE, erule (1) notE impE)
   7.217 -apply (erule exE, rename_tac delta)
   7.218 -apply (erule_tac x = delta in allE)
   7.219 -apply (subgoal_tac "N1 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> delta")
   7.220 - apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym])
   7.221 -apply (simp add: subst_eq_iff)
   7.222 -done
   7.223 -
   7.224 -
   7.225 -text{*Unify returns idempotent substitutions, when it succeeds.*}
   7.226 -theorem unify_gives_Idem [rule_format]:
   7.227 -     "\<forall>theta. unify(M,N) = Some theta --> Idem theta"
   7.228 -apply (rule_tac u = M and v = N in unify_induct0)
   7.229 -apply (simp_all add: Var_Idem unify_tc2 split add: option.split)
   7.230 -txt{*Comb-Comb case*}
   7.231 -apply safe
   7.232 -apply (drule spec, erule (1) notE impE)+
   7.233 -apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def])
   7.234 -apply (rule Idem_comp, assumption+)
   7.235 -apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def)
   7.236 -done
   7.237 -
   7.238 -end