# HG changeset patch
# User paulson
# Date 1112382240 -7200
# Node ID f6da795ee27abc93bb13ed24680beec18028ec52
# Parent  b1f486a9c56b94433c124cccd2db1d8df5c30323
x-symbols and other tidying

diff -r b1f486a9c56b -r f6da795ee27a src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Fri Apr 01 18:59:17 2005 +0200
+++ b/src/HOL/Subst/Subst.thy	Fri Apr 01 21:04:00 2005 +0200
@@ -20,70 +20,80 @@
   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)
+
+
 primrec
-  subst_Var:      "(Var v <| s) = assoc v (Var v) s"
-  subst_Const:  "(Const c <| s) = Const c"
-  subst_Comb:  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
+  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 <| r = t <| s"
+  subst_eq_def:  "r =$= s == ALL t. t \<lhd> r = t \<lhd> s"
 
-  comp_def:    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
+  comp_def:    "al \<lozenge> bl == alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
 
   sdom_def:
   "sdom(al) == alist_rec al {}  
                 (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
 
   srange_def:
-   "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
+   "srange(al) == Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})"
 
 
 
 subsection{*Basic Laws*}
 
-lemma subst_Nil [simp]: "t <| [] = t"
+lemma subst_Nil [simp]: "t \<lhd> [] = t"
 by (induct_tac "t", auto)
 
-lemma subst_mono [rule_format]: "t <: u --> t <| s <: u <| s"
+lemma subst_mono [rule_format]: "t \<prec> u --> t \<lhd> s \<prec> u \<lhd> s"
 by (induct_tac "u", auto)
 
 lemma Var_not_occs [rule_format]:
-     "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"
+     "~ (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 = "%x.~x=Var (v) --> ~ (Var (v) <: x) --> x <| (v,t<|s) #s=x<|s" in uterm.induct)
+apply (rule_tac [2] 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
 
-lemma agreement: "(t <|r = t <|s) = (\<forall>v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"
+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)
 
-lemma repl_invariance: "~ v: vars_of(t) ==> t <| (v,u)#s = t <| s"
+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 : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"
+     "v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)"
 by (induct_tac "t", auto)
 
 
 subsection{*Equality between Substitutions*}
 
-lemma subst_eq_iff: "r =$= s = (\<forall>t. t <| r = t <| s)"
+lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)"
 by (simp add: subst_eq_def)
 
-lemma subst_refl [iff]: "r =$= r"
+lemma subst_refl [iff]: "r \<doteq> r"
 by (simp add: subst_eq_iff)
 
-lemma subst_sym: "r =$= s ==> s =$= r"
+lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
 by (simp add: subst_eq_iff)
 
-lemma subst_trans: "[| q =$= r; r =$= s |] ==> q =$= s"
+lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
 by (simp add: subst_eq_iff)
 
 lemma subst_subst2:
-    "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)"
+    "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
 by (simp add: subst_eq_def)
 
 lemmas ssubst_subst2 = subst_sym [THEN subst_subst2]
@@ -92,98 +102,95 @@
 subsection{*Composition of Substitutions*}
 
 lemma [simp]: 
-     "[] <> bl = bl"
-     "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)"
+     "[] \<lozenge> bl = bl"
+     "((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) 
 
-lemma comp_Nil [simp]: "s <> [] = s"
+lemma comp_Nil [simp]: "s \<lozenge> [] = s"
 by (induct "s", auto)
 
-lemma subst_comp_Nil: "s =$= s <> []"
+lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []"
 by simp
 
-lemma subst_comp [simp]: "(t <| r <> s) = (t <| r <| s)"
+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
 
-lemma comp_assoc: "(q <> r) <> s =$= q <> (r <> s)"
-apply (simp (no_asm) add: subst_eq_iff)
-done
+lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)"
+by (simp add: subst_eq_iff)
 
 lemma subst_cong:
-     "[| theta =$= theta1; sigma =$= sigma1|] 
-      ==> (theta <> sigma) =$= (theta1 <> sigma1)"
+     "[| 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) <| s) # s =$= s"
+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
 
 
-lemma comp_subst_subst: "q <> r =$= s ==>  t <| q <| r = t <| s"
+lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==>  t \<lhd> q \<lhd> r = t \<lhd> s"
 by (simp add: subst_eq_iff)
 
 
 subsection{*Domain and range of Substitutions*}
 
-lemma sdom_iff: "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"
+lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
 apply (induct "s")
 apply (case_tac [2] a, auto)  
 done
 
 
 lemma srange_iff: 
-   "v : srange(s) = (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))"
+   "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)
 
-lemma invariance: "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"
+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
 
 lemma Var_in_srange [rule_format]:
-     "v : sdom(s) -->  v : vars_of(t <| s) --> v : srange(s)"
+     "v \<in> sdom(s) -->  v \<in> vars_of(t \<lhd> s) --> v \<in> srange(s)"
 apply (induct_tac "t")
-apply (case_tac "a : sdom (s) ")
+apply (case_tac "a \<in> sdom s")
 apply (auto simp add: sdom_iff srange_iff)
 done
 
-lemma Var_elim: "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)"
+lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==>  v \<notin> vars_of(t \<lhd> s)"
 by (blast intro: Var_in_srange)
 
 lemma Var_intro [rule_format]:
-     "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"
+     "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 srangeD [rule_format]:
-     "v : srange(s) --> (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))"
-apply (simp (no_asm) add: srange_iff)
-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)
 
 lemma dom_range_disjoint:
-     "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t <| s) = {})"
-apply (simp (no_asm) add: empty_iff_all_not)
+     "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 <| s = u ==> (\<exists>x. x : sdom(s))"
+lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))"
 by (auto simp add: empty_iff_all_not invariance)
 
 
-lemma id_subst_lemma [simp]: "(M <| [(x, Var x)]) = M"
+lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
 by (induct_tac "M", auto)
 
 
diff -r b1f486a9c56b -r f6da795ee27a src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Fri Apr 01 18:59:17 2005 +0200
+++ b/src/HOL/Subst/UTerm.thy	Fri Apr 01 21:04:00 2005 +0200
@@ -19,7 +19,10 @@
 consts
   vars_of  ::  "'a uterm => 'a set"
   "<:"     ::  "'a uterm => 'a uterm => bool"   (infixl 54) 
-uterm_size ::  "'a uterm => nat"
+  uterm_size ::  "'a uterm => nat"
+
+syntax (xsymbols)
+  "op <:"     ::  "'a uterm => 'a uterm => bool"   (infixl "\<prec>" 54) 
 
 
 primrec
@@ -27,11 +30,10 @@
   vars_of_Const: "vars_of (Const c) = {}"
   vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
 
-
 primrec
-  occs_Var:   "u <: (Var v) = False"
-  occs_Const: "u <: (Const c) = False"
-  occs_Comb:  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
+  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)"
 
 primrec
   uterm_size_Var:   "uterm_size (Var v) = 0"
@@ -39,19 +41,20 @@
   uterm_size_Comb:  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
 
 
-lemma vars_var_iff: "(v : vars_of(Var(w))) = (w=v)"
+lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
 by auto
 
-lemma vars_iff_occseq: "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"
+lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
 by (induct_tac "t", auto)
 
 
-(* Not used, but perhaps useful in other proofs *)
-lemma occs_vars_subset: "M<:N --> vars_of(M) <= vars_of(N)"
+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 monotone_vars_of: "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"
+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
 
 lemma finite_vars_of: "finite(vars_of M)"
diff -r b1f486a9c56b -r f6da795ee27a src/HOL/Subst/Unify.thy
--- a/src/HOL/Subst/Unify.thy	Fri Apr 01 18:59:17 2005 +0200
+++ b/src/HOL/Subst/Unify.thy	Fri Apr 01 21:04:00 2005 +0200
@@ -11,12 +11,12 @@
 begin
 
 text{*
-Substitution and Unification in Higher-Order Logic. 
+Substitution and Unification in Higher-Order Logic.
 
 Implements Manna and Waldinger's formalization, with Paulson's simplifications,
 and some new simplifications by Slind.
 
-Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm. 
+Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm.
 SCP 1 (1981), 5-48
 
 L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
@@ -32,7 +32,7 @@
        "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, 
+         either the set of variables decreases,
          or the first argument does (in fact, both do) *}
 
 text{* Wellfoundedness of unifyRel *}
@@ -44,39 +44,38 @@
  unify_CC: "unify(Const m, Const n)  = (if (m=n) then Some[] else None)"
  unify_CB: "unify(Const m, Comb M N) = None"
  unify_CV: "unify(Const m, Var v)    = Some[(v,Const m)]"
- unify_V:  "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])"
+ unify_V:  "unify(Var v, M) = (if (Var v \<prec> M) then None else Some[(v,M)])"
  unify_BC: "unify(Comb M N, Const x) = None"
- unify_BV: "unify(Comb M N, Var v)   = (if (Var v <: Comb M N) then None   
+ unify_BV: "unify(Comb M N, Var v)   = (if (Var v \<prec> Comb M N) then None
                                         else Some[(v,Comb M N)])"
  unify_BB:
-  "unify(Comb M1 N1, Comb M2 N2) =   
-      (case unify(M1,M2)  
-        of None       => None  
-         | Some theta => (case unify(N1 <| theta, N2 <| theta)  
-                            of None       => None  
-                             | Some sigma => Some (theta <> sigma)))"
+  "unify(Comb M1 N1, Comb M2 N2) =
+      (case unify(M1,M2)
+        of None       => None
+         | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta)
+                            of None       => None
+                             | Some sigma => Some (theta \<lozenge> sigma)))"
   (hints recdef_wf: wf_unifyRel)
 
 
+text{* This file defines a nested unification algorithm, then proves that it
+ terminates, then proves 2 correctness theorems: that when the algorithm
+ succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
+ Although the proofs may seem long, they are actually quite direct, in that
+ the correctness and termination properties are not mingled as much as in
+ previous proofs of this algorithm.*}
 
 (*---------------------------------------------------------------------------
- * This file defines a nested unification algorithm, then proves that it 
- * terminates, then proves 2 correctness theorems: that when the algorithm
- * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
- * Although the proofs may seem long, they are actually quite direct, in that
- * the correctness and termination properties are not mingled as much as in 
- * previous proofs of this algorithm. 
- *
- * Our approach for nested recursive functions is as follows: 
+ * Our approach for nested recursive functions is as follows:
  *
  *    0. Prove the wellfoundedness of the termination relation.
  *    1. Prove the non-nested termination conditions.
- *    2. Eliminate (0) and (1) from the recursion equations and the 
+ *    2. Eliminate (0) and (1) from the recursion equations and the
  *       induction theorem.
- *    3. Prove the nested termination conditions by using the induction 
- *       theorem from (2) and by using the recursion equations from (2). 
- *       These are constrained by the nested termination conditions, but 
- *       things work out magically (by wellfoundedness of the termination 
+ *    3. Prove the nested termination conditions by using the induction
+ *       theorem from (2) and by using the recursion equations from (2).
+ *       These are constrained by the nested termination conditions, but
+ *       things work out magically (by wellfoundedness of the termination
  *       relation).
  *    4. Eliminate the nested TCs from the results of (2).
  *    5. Prove further correctness properties using the results of (4).
@@ -84,17 +83,15 @@
  * Deeper nestings require iteration of steps (3) and (4).
  *---------------------------------------------------------------------------*)
 
-text{*The non-nested TC (terminiation condition). This declaration form
-only seems to return one subgoal outstanding from the recdef.*}
-recdef_tc unify_tc1: unify
+text{*The non-nested TC (terminiation condition).*}
+recdef_tc unify_tc1: unify (1)
 apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
-apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def)
+apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def
+                 inv_image_def)
 apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
 done
 
 
-
-
 text{*Termination proof.*}
 
 lemma trans_unifyRel: "trans unifyRel"
@@ -105,21 +102,21 @@
 text{*The following lemma is used in the last step of the termination proof
 for the nested call in Unify.  Loosely, it says that unifyRel doesn't care
 about term structure.*}
-lemma Rassoc: 
-  "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==>  
-   ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel"
-by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc 
+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: measure_def less_eq inv_image_def add_assoc Un_assoc
               unifyRel_def lex_prod_def)
 
 
-text{*This lemma proves the nested termination condition for the base cases 
+text{*This lemma proves the nested termination condition for the base cases
  * 3, 4, and 6.*}
 lemma var_elimR:
-  "~(Var x <: M) ==>  
-    ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel  
-  & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel"
+  "~(Var x \<prec> M) ==>
+    ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel
+  & ((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: (vars_of N1 Un vars_of N2) ")
+apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
 txt{*uterm_less case*}
 apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def)
 apply blast
@@ -127,10 +124,11 @@
 apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def)
 apply (simp add: finite_psubset_def finite_vars_of psubset_def)
 apply blast
-txt{*Final case, also {text finite_psubset}*}
-apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def)
-apply (cut_tac s = "[ (x,M) ]" and v = x and t = N2 in Var_elim)
-apply (cut_tac [3] s = "[ (x,M) ]" and v = x and t = N1 in Var_elim)
+txt{*Final case, also @{text finite_psubset}*}
+apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def
+                 measure_def inv_image_def)
+apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim)
+apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim)
 apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
 apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff)
 done
@@ -138,30 +136,28 @@
 
 text{*Eliminate tc1 from the recursion equations and the induction theorem.*}
 
-lemmas unify_nonrec [simp] = 
-       unify_CC unify_CB unify_CV unify_V unify_BC unify_BV 
+lemmas unify_nonrec [simp] =
+       unify_CC unify_CB unify_CV unify_V unify_BC unify_BV
 
 lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1]
 
 lemmas unify_induct0 = unify.induct [OF unify_tc1]
 
-text{*The nested TC. Proved by recursion induction.*}
-lemma unify_tc2:
-     "\<forall>M1 M2 N1 N2 theta.
-       unify (M1, M2) = Some theta \<longrightarrow>
-       ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) \<in> unifyRel"
+text{*The nested TC. The (2) requests the second one.
+      Proved by recursion induction.*}
+recdef_tc unify_tc2: unify (2)
 txt{*The extracted TC needs the scope of its quantifiers adjusted, so our
  first step is to restrict the scopes of N1 and N2.*}
-apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta --> 
-      (\<forall>N1 N2.((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)")
+apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta -->
+      (\<forall>N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> unifyRel)")
 apply blast
 apply (rule allI)
 apply (rule allI)
 txt{*Apply induction on this still-quantified formula*}
 apply (rule_tac u = M1 and v = M2 in unify_induct0)
-apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
-txt{*Const-Const case*}
-apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq)
+      apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
+ txt{*Const-Const case*}
+ apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq)
 txt{*Comb-Comb case*}
 apply (simp (no_asm_simp) split add: option.split)
 apply (intro strip)
@@ -175,12 +171,12 @@
 
 text{*Desired rule, copied from the theory file.*}
 lemma unifyCombComb [simp]:
-    "unify(Comb M1 N1, Comb M2 N2) =       
-       (case unify(M1,M2)                
-         of None => None                 
-          | Some theta => (case unify(N1 <| theta, N2 <| theta)         
-                             of None => None     
-                              | Some sigma => Some (theta <> sigma)))"
+    "unify(Comb M1 N1, Comb M2 N2) =
+       (case unify(M1,M2)
+         of None => None
+          | Some theta => (case unify(N1 \<lhd> theta, N2 \<lhd> theta)
+                             of None => None
+                              | Some sigma => Some (theta \<lozenge> sigma)))"
 by (simp add: unify_tc2 unify_simps0 split add: option.split)
 
 text{*The ML version had this, but it can't be used: we get
@@ -202,20 +198,19 @@
 theorem unify_gives_MGU [rule_format]:
      "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N"
 apply (rule_tac u = M and v = N in unify_induct0)
-apply (simp_all (no_asm_simp))
-(*Const-Const case*)
-apply (simp (no_asm) add: MGUnifier_def Unifier_def)
-(*Const-Var case*)
-apply (subst mgu_sym)
-apply (simp (no_asm) add: MGUnifier_Var)
-(*Var-M case*)
-apply (simp (no_asm) add: MGUnifier_Var)
-(*Comb-Var case*)
-apply (subst mgu_sym)
-apply (simp (no_asm) add: MGUnifier_Var)
-(** LEVEL 8 **)
-(*Comb-Comb case*)
-apply (simp add: unify_tc2) 
+    apply (simp_all (no_asm_simp))
+    txt{*Const-Const case*}
+    apply (simp add: MGUnifier_def Unifier_def)
+   txt{*Const-Var case*}
+   apply (subst mgu_sym)
+   apply (simp add: MGUnifier_Var)
+  txt{*Var-M case*}
+  apply (simp add: MGUnifier_Var)
+ txt{*Comb-Var case*}
+ apply (subst mgu_sym)
+ apply (simp add: MGUnifier_Var)
+txt{*Comb-Comb case*}
+apply (simp add: unify_tc2)
 apply (simp (no_asm_simp) split add: option.split)
 apply (intro strip)
 apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def)
@@ -223,9 +218,9 @@
 apply (erule_tac x = gamma in allE, erule (1) notE impE)
 apply (erule exE, rename_tac delta)
 apply (erule_tac x = delta in allE)
-apply (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta")
+apply (subgoal_tac "N1 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> delta")
  apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym])
-apply (simp add: subst_eq_iff) 
+apply (simp add: subst_eq_iff)
 done