--- 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
--- 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
--- 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
--- 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
--- 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*}