# HG changeset patch
# User wenzelm
# Date 1191432965 -7200
# Node ID bfb619994060a8946f8b4c8e393144e69e6891e4
# Parent  b854842e0b8d92da58edc6f0f2d2c644a873bf26
modernized specifications;
tuned proofs;

diff -r b854842e0b8d -r bfb619994060 src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Wed Oct 03 00:03:01 2007 +0200
+++ b/src/HOL/Subst/AList.thy	Wed Oct 03 19:36:05 2007 +0200
@@ -10,22 +10,19 @@
 imports Main
 begin
 
-consts
-  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
-  assoc      :: "['a,'b,('a*'b) list] => 'b"
-
+consts alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
 primrec
   "alist_rec [] c d = c"
   "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
 
+consts assoc      :: "['a,'b,('a*'b) list] => 'b"
 primrec
   "assoc v d [] = d"
   "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
 
-
 lemma alist_induct:
     "[| P([]);    
         !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
-by (induct_tac "l", auto)
+  by (induct l) auto
 
 end
diff -r b854842e0b8d -r bfb619994060 src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Wed Oct 03 00:03:01 2007 +0200
+++ b/src/HOL/Subst/Subst.thy	Wed Oct 03 19:36:05 2007 +0200
@@ -11,92 +11,87 @@
 begin
 
 consts
-
-  "=$="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
-  "<|"   ::  "'a uterm => ('a * 'a uterm) list => 'a uterm"        (infixl 55)
-  "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list] 
-                 => ('a*('a uterm)) list"                          (infixl 56)
-  sdom   ::  "('a*('a uterm)) list => 'a set"
-  srange ::  "('a*('a uterm)) list => 'a set"
-
-
-syntax (xsymbols)
-  "op =$=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" 
-              (infixr "\<doteq>" 52)
-  "op <|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "\<lhd>" 55)
-  "op <>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] 
-                 => ('a*('a uterm)) list"                   (infixl "\<lozenge>" 56)
-
-
+  subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm"  (infixl "<|" 55)
+notation (xsymbols)
+  subst  (infixl "\<lhd>" 55)
 primrec
   subst_Var:      "(Var v \<lhd> s) = assoc v (Var v) s"
   subst_Const:  "(Const c \<lhd> s) = Const c"
   subst_Comb:  "(Comb M N \<lhd> s) = Comb (M \<lhd> s) (N \<lhd> s)"
 
-
-defs 
-
-  subst_eq_def:  "r =$= s == ALL t. t \<lhd> r = t \<lhd> s"
-
-  comp_def:    "al \<lozenge> bl == alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
+definition
+  subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"  (infixr "=$=" 52) where
+  "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+notation
+  subst_eq  (infixr "\<doteq>" 52)
 
-  sdom_def:
-  "sdom(al) == alist_rec al {}  
-                (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
+definition
+  comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
+    (infixl "<>" 56) where
+  "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
+notation
+  comp  (infixl "\<lozenge>" 56)
 
-  srange_def:
-   "srange(al) == Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})"
+definition
+  sdom :: "('a*('a uterm)) list => 'a set" where
+  "sdom al = alist_rec al {} (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
+
+definition
+  srange :: "('a*('a uterm)) list => 'a set" where
+  "srange al = Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})"
 
 
 
 subsection{*Basic Laws*}
 
 lemma subst_Nil [simp]: "t \<lhd> [] = t"
-by (induct_tac "t", auto)
+  by (induct t) auto
 
-lemma subst_mono [rule_format]: "t \<prec> u --> t \<lhd> s \<prec> u \<lhd> s"
-by (induct_tac "u", auto)
+lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
+  by (induct u) auto
 
-lemma Var_not_occs [rule_format]:
-     "~ (Var(v) \<prec> t) --> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s"
-apply (case_tac "t = Var v")
-apply (erule_tac [2] rev_mp)
-apply (rule_tac [2] P = 
+lemma Var_not_occs: "~ (Var(v) \<prec> t) \<Longrightarrow> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s"
+  apply (case_tac "t = Var v")
+   prefer 2
+   apply (erule rev_mp)+
+   apply (rule_tac P =
          "%x. x \<noteq> Var v --> ~(Var v \<prec> x) --> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s" 
        in uterm.induct)
-apply auto 
-done
+     apply auto
+  done
 
 lemma agreement: "(t\<lhd>r = t\<lhd>s) = (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
-by (induct_tac "t", auto)
+  by (induct t) auto
 
-lemma repl_invariance: "~ v: vars_of(t) ==> t \<lhd> (v,u)#s = t \<lhd> s"
-by (simp add: agreement)
+lemma repl_invariance: "~ v: vars_of t ==> t \<lhd> (v,u)#s = t \<lhd> s"
+  by (simp add: agreement)
 
-lemma Var_in_subst [rule_format]:
-     "v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)"
-by (induct_tac "t", auto)
+lemma Var_in_subst:
+    "v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)"
+  by (induct t) auto
 
 
 subsection{*Equality between Substitutions*}
 
 lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)"
-by (simp add: subst_eq_def)
+  by (simp add: subst_eq_def)
 
 lemma subst_refl [iff]: "r \<doteq> r"
-by (simp add: subst_eq_iff)
+  by (simp add: subst_eq_iff)
 
 lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
-by (simp add: subst_eq_iff)
+  by (simp add: subst_eq_iff)
 
 lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
-by (simp add: subst_eq_iff)
+  by (simp add: subst_eq_iff)
 
 lemma subst_subst2:
     "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
-by (simp add: subst_eq_def)
+  by (simp add: subst_eq_def)
 
-lemmas ssubst_subst2 = subst_sym [THEN subst_subst2]
+lemma ssubst_subst2:
+    "[| s \<doteq> r; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
+  by (simp add: subst_eq_def)
 
 
 subsection{*Composition of Substitutions*}
@@ -106,92 +101,95 @@
      "((a,b)#al) \<lozenge> bl = (a,b \<lhd> bl) # (al \<lozenge> bl)"
      "sdom([]) = {}"
      "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"
-by (simp_all add: comp_def sdom_def) 
+  by (simp_all add: comp_def sdom_def) 
 
 lemma comp_Nil [simp]: "s \<lozenge> [] = s"
-by (induct "s", auto)
+  by (induct s) auto
 
 lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []"
-by simp
+  by simp
 
 lemma subst_comp [simp]: "(t \<lhd> r \<lozenge> s) = (t \<lhd> r \<lhd> s)"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-apply (induct "r", auto)
-done
+  apply (induct t)
+  apply simp_all
+  apply (induct r)
+   apply auto
+  done
 
 lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)"
-by (simp add: subst_eq_iff)
+  by (simp add: subst_eq_iff)
 
 lemma subst_cong:
-     "[| theta \<doteq> theta1; sigma \<doteq> sigma1|] 
-      ==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)"
-by (simp add: subst_eq_def)
+  "[| theta \<doteq> theta1; sigma \<doteq> sigma1|] 
+    ==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)"
+  by (simp add: subst_eq_def)
 
 
 lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s"
-apply (simp add: subst_eq_iff)
-apply (rule allI)
-apply (induct_tac "t", simp_all)
-done
+  apply (simp add: subst_eq_iff)
+  apply (rule allI)
+  apply (induct_tac t)
+    apply simp_all
+  done
 
 
 lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==>  t \<lhd> q \<lhd> r = t \<lhd> s"
-by (simp add: subst_eq_iff)
+  by (simp add: subst_eq_iff)
 
 
 subsection{*Domain and range of Substitutions*}
 
 lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
-apply (induct "s")
-apply (case_tac [2] a, auto)  
-done
+  apply (induct s)
+   apply (case_tac [2] a)
+   apply auto
+  done
 
 
 lemma srange_iff: 
-   "v \<in> srange(s) = (\<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s))"
-by (auto simp add: srange_def)
+    "v \<in> srange(s) = (\<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s))"
+  by (auto simp add: srange_def)
 
 lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
-by (unfold empty_def, blast)
+  unfolding empty_def by blast
 
 lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})"
-apply (induct_tac "t")
-apply (auto simp add: empty_iff_all_not sdom_iff)
-done
+  apply (induct t)
+    apply (auto simp add: empty_iff_all_not sdom_iff)
+  done
 
-lemma Var_in_srange [rule_format]:
-     "v \<in> sdom(s) -->  v \<in> vars_of(t \<lhd> s) --> v \<in> srange(s)"
-apply (induct_tac "t")
-apply (case_tac "a \<in> sdom s")
-apply (auto simp add: sdom_iff srange_iff)
-done
+lemma Var_in_srange:
+    "v \<in> sdom(s) \<Longrightarrow>  v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s)"
+  apply (induct t)
+    apply (case_tac "a \<in> sdom s")
+  apply (auto simp add: sdom_iff srange_iff)
+  done
 
 lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==>  v \<notin> vars_of(t \<lhd> s)"
-by (blast intro: Var_in_srange)
+  by (blast intro: Var_in_srange)
 
-lemma Var_intro [rule_format]:
-     "v \<in> vars_of(t \<lhd> s) --> v \<in> srange(s) | v \<in> vars_of(t)"
-apply (induct_tac "t")
-apply (auto simp add: sdom_iff srange_iff)
-apply (rule_tac x=a in exI, auto) 
-done
+lemma Var_intro:
+    "v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s) | v \<in> vars_of(t)"
+  apply (induct t)
+    apply (auto simp add: sdom_iff srange_iff)
+  apply (rule_tac x=a in exI)
+  apply auto 
+  done
 
 lemma srangeD: "v \<in> srange(s) ==> \<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s)"
-by (simp add: srange_iff)
+  by (simp add: srange_iff)
 
 lemma dom_range_disjoint:
-     "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t \<lhd> s) = {})"
-apply (simp add: empty_iff_all_not)
-apply (force intro: Var_in_srange dest: srangeD)
-done
+    "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t \<lhd> s) = {})"
+  apply (simp add: empty_iff_all_not)
+  apply (force intro: Var_in_srange dest: srangeD)
+  done
 
 lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))"
-by (auto simp add: empty_iff_all_not invariance)
+  by (auto simp add: empty_iff_all_not invariance)
 
 
 lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
-by (induct_tac "M", auto)
-
+  by (induct M) auto
 
 end
diff -r b854842e0b8d -r bfb619994060 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Wed Oct 03 00:03:01 2007 +0200
+++ b/src/HOL/Subst/UTerm.thy	Wed Oct 03 19:36:05 2007 +0200
@@ -7,34 +7,31 @@
 
 theory UTerm
 imports Main
-
 begin
 
 text{*Binary trees with leaves that are constants or variables.*}
 
-datatype 'a uterm = Var 'a
-                  | Const 'a
-                  | Comb "'a uterm" "'a uterm"
+datatype 'a uterm =
+    Var 'a
+  | Const 'a
+  | Comb "'a uterm" "'a uterm"
 
-consts
-  vars_of  ::  "'a uterm => 'a set"
-  "<:"     ::  "'a uterm => 'a uterm => bool"   (infixl 54) 
-  uterm_size ::  "'a uterm => nat"
-
-syntax (xsymbols)
-  "op <:"     ::  "'a uterm => 'a uterm => bool"   (infixl "\<prec>" 54) 
-
-
+consts vars_of :: "'a uterm => 'a set"
 primrec
   vars_of_Var:   "vars_of (Var v) = {v}"
   vars_of_Const: "vars_of (Const c) = {}"
   vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
 
+consts occs :: "'a uterm => 'a uterm => bool"   (infixl "<:" 54) 
+notation (xsymbols)
+  occs  (infixl "\<prec>" 54)
 primrec
   occs_Var:   "u \<prec> (Var v) = False"
   occs_Const: "u \<prec> (Const c) = False"
   occs_Comb:  "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
 
+consts
+  uterm_size ::  "'a uterm => nat"
 primrec
   uterm_size_Var:   "uterm_size (Var v) = 0"
   uterm_size_Const: "uterm_size (Const c) = 0"
@@ -42,23 +39,22 @@
 
 
 lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
-by auto
+  by auto
 
 lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
-by (induct_tac "t", auto)
+  by (induct t) auto
 
 
 text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset [rule_format]: "M\<prec>N --> vars_of(M) \<subseteq> vars_of(N)"
-by (induct_tac "N", auto)
+lemma occs_vars_subset: "M\<prec>N \<Longrightarrow> vars_of(M) \<subseteq> vars_of(N)"
+  by (induct N) auto
 
 
 lemma monotone_vars_of:
-     "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
-by blast
+    "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
+  by blast
 
 lemma finite_vars_of: "finite(vars_of M)"
-by (induct_tac "M", auto)
-
+  by (induct M) auto
 
 end
diff -r b854842e0b8d -r bfb619994060 src/HOL/Subst/Unifier.thy
--- a/src/HOL/Subst/Unifier.thy	Wed Oct 03 00:03:01 2007 +0200
+++ b/src/HOL/Subst/Unifier.thy	Wed Oct 03 19:36:05 2007 +0200
@@ -8,24 +8,23 @@
 
 theory Unifier
 imports Subst
-
 begin
 
-consts
+definition
+  Unifier   :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
+  "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
 
-  Unifier   :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool"
-  ">>"      :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr 52)
-  MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool"
-  Idem      :: "('a * 'a uterm)list => bool"
+definition
+  MoreGeneral :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr ">>" 52) where
+  "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
 
-defs
+definition
+  MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
+  "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
 
-  Unifier_def:      "Unifier s t u == t <| s = u <| s"
-  MoreGeneral_def:  "r >> s == ? q. s =$= r <> q"
-  MGUnifier_def:    "MGUnifier s t u == Unifier s t u & 
-                                        (!r. Unifier r t u --> s >> r)"
-  Idem_def:         "Idem(s) == (s <> s) =$= s"
-
+definition
+  Idem :: "('a * 'a uterm)list => bool" where
+  "Idem s \<longleftrightarrow> (s <> s) =$= s"
 
 
 lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
@@ -34,62 +33,59 @@
 subsection{*Unifiers*}
 
 lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
-by (simp add: Unifier_def)
+  by (simp add: Unifier_def)
 
 
 lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
-by (simp add: Unifier_def repl_invariance)
+  by (simp add: Unifier_def repl_invariance)
 
 
 subsection{* Most General Unifiers*}
 
 lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
-by (simp add: unify_defs eq_commute)
+  by (simp add: unify_defs eq_commute)
 
 
 lemma MoreGen_Nil [iff]: "[] >> s"
-by (auto simp add: MoreGeneral_def)
+  by (auto simp add: MoreGeneral_def)
 
 lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"
-apply (unfold unify_defs)
-apply (auto intro: ssubst_subst2 subst_comp_Nil)
-done
+  apply (unfold unify_defs)
+  apply (auto intro: ssubst_subst2 subst_comp_Nil)
+  done
 
-lemma MGUnifier_Var: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
-apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
-apply safe
-apply (rule exI)
-apply (erule subst, rule Cons_trivial [THEN subst_sym])
-apply (erule ssubst_subst2)
-apply (simp (no_asm_simp) add: Var_not_occs)
-done
-
-declare MGUnifier_Var [intro!]
+lemma MGUnifier_Var [intro!]: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
+  apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
+  apply safe
+   apply (rule exI)
+   apply (erule subst, rule Cons_trivial [THEN subst_sym])
+  apply (erule ssubst_subst2)
+  apply (simp (no_asm_simp) add: Var_not_occs)
+  done
 
 
 subsection{*Idempotence*}
 
 lemma Idem_Nil [iff]: "Idem([])"
-by (simp add: Idem_def)
+  by (simp add: Idem_def)
 
 lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
-by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
+  by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
 
 lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
-by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
+  by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
 
 lemma Unifier_Idem_subst: 
   "[| Idem(r); Unifier s (t<|r) (u<|r) |]  
-   ==> Unifier (r <> s) (t <| r) (u <| r)"
-by (simp add: Idem_def Unifier_def comp_subst_subst)
+    ==> Unifier (r <> s) (t <| r) (u <| r)"
+  by (simp add: Idem_def Unifier_def comp_subst_subst)
 
 lemma Idem_comp:
-     "[| Idem(r);  Unifier s (t <| r) (u <| r);  
-         !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q  
-      |] ==> Idem(r <> s)"
-apply (frule Unifier_Idem_subst, blast) 
-apply (force simp add: Idem_def subst_eq_iff)
-done
-
+  "[| Idem(r);  Unifier s (t <| r) (u <| r);  
+      !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q  
+    |] ==> Idem(r <> s)"
+  apply (frule Unifier_Idem_subst, blast) 
+  apply (force simp add: Idem_def subst_eq_iff)
+  done
 
 end
diff -r b854842e0b8d -r bfb619994060 src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Wed Oct 03 00:03:01 2007 +0200
+++ b/src/HOL/Subst/Unify.thy	Wed Oct 03 19:36:05 2007 +0200
@@ -26,24 +26,20 @@
 L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
 *}
 
-consts
-
-   unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
-   unify    :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
-
-defs
-  unifyRel_def:
-       "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
-                               (%(M,N). (vars_of M Un vars_of N, M))"
+definition
+   unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
+  "unifyRel = inv_image (finite_psubset <*lex*> measure uterm_size)
+      (%(M,N). (vars_of M Un vars_of N, M))"
    --{*Termination relation for the Unify function:
          either the set of variables decreases,
          or the first argument does (in fact, both do) *}
 
+
 text{* Wellfoundedness of unifyRel *}
 lemma wf_unifyRel [iff]: "wf unifyRel"
-by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
+  by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
 
-
+consts unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
 recdef (permissive) unify "unifyRel"
  unify_CC: "unify(Const m, Const n)  = (if (m=n) then Some[] else None)"
  unify_CB: "unify(Const m, Comb M N) = None"
@@ -95,8 +91,8 @@
 text{*Termination proof.*}
 
 lemma trans_unifyRel: "trans unifyRel"
-by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
-              trans_finite_psubset)
+  by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
+    trans_finite_psubset)
 
 
 text{*The following lemma is used in the last step of the termination proof
@@ -104,9 +100,8 @@
 about term structure.*}
 lemma Rassoc:
   "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel  ==>
-   ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
-by (simp add: less_eq add_assoc Un_assoc
-              unifyRel_def lex_prod_def)
+    ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
+  by (simp add: less_eq add_assoc Un_assoc unifyRel_def lex_prod_def)
 
 
 text{*This lemma proves the nested termination condition for the base cases
@@ -117,7 +112,7 @@
   & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel"
 apply (case_tac "Var x = M", clarify, simp)
 apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
-txt{*uterm_less case*}
+txt{*@{text uterm_less} case*}
 apply (simp add: less_eq unifyRel_def lex_prod_def)
 apply blast
 txt{*@{text finite_psubset} case*}