author krauss Tue, 21 Apr 2009 09:53:31 +0200 changeset 30909 bd4f255837e5 parent 30908 7ccf4a3d764c child 30921 fbdefa2196fa child 30958 d8a30cdae862 child 31105 95f66b234086
tuned proof
```--- a/src/HOL/ex/Unification.thy	Tue Apr 21 09:53:27 2009 +0200
+++ b/src/HOL/ex/Unification.thy	Tue Apr 21 09:53:31 2009 +0200
@@ -277,7 +277,7 @@
by (induct t) simp_all
qed

-lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
+lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)"
proof
assume t_v: "t = Var v"
thus "[(v, t)] =\<^sub>s []"
@@ -307,7 +307,7 @@
proof cases
assume "v = x"
thus ?thesis
-      by (simp add:var_same[symmetric])
+      by (simp add:var_same)
next
assume neq: "v \<noteq> x"
have "elim [(v, Var x)] v"
@@ -328,13 +328,13 @@
by auto

from nonocc have "\<not> [(v,M)] =\<^sub>s []"
-    by (simp add:var_same[symmetric])
+    by (simp add:var_same)
with ih1 have "elim [(v, M)] v" by blast
hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
hence not_in_M: "v \<notin> vars_of M" by simp

from nonocc have "\<not> [(v,N)] =\<^sub>s []"
-    by (simp add:var_same[symmetric])
+    by (simp add:var_same)
with ih2 have "elim [(v, N)] v" by blast
hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
hence not_in_N: "v \<notin> vars_of N" by simp```