tuned proof
authorkrauss
Tue Apr 21 09:53:31 2009 +0200 (2009-04-21)
changeset 30909bd4f255837e5
parent 30908 7ccf4a3d764c
child 30921 fbdefa2196fa
child 30958 d8a30cdae862
child 31105 95f66b234086
tuned proof
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/Unification.thy	Tue Apr 21 09:53:27 2009 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Tue Apr 21 09:53:31 2009 +0200
     1.3 @@ -277,7 +277,7 @@
     1.4      by (induct t) simp_all
     1.5  qed
     1.6  
     1.7 -lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
     1.8 +lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)"
     1.9  proof
    1.10    assume t_v: "t = Var v"
    1.11    thus "[(v, t)] =\<^sub>s []"
    1.12 @@ -307,7 +307,7 @@
    1.13    proof cases
    1.14      assume "v = x"
    1.15      thus ?thesis
    1.16 -      by (simp add:var_same[symmetric])
    1.17 +      by (simp add:var_same)
    1.18    next
    1.19      assume neq: "v \<noteq> x"
    1.20      have "elim [(v, Var x)] v"
    1.21 @@ -328,13 +328,13 @@
    1.22      by auto
    1.23  
    1.24    from nonocc have "\<not> [(v,M)] =\<^sub>s []"
    1.25 -    by (simp add:var_same[symmetric])
    1.26 +    by (simp add:var_same)
    1.27    with ih1 have "elim [(v, M)] v" by blast
    1.28    hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
    1.29    hence not_in_M: "v \<notin> vars_of M" by simp
    1.30  
    1.31    from nonocc have "\<not> [(v,N)] =\<^sub>s []"
    1.32 -    by (simp add:var_same[symmetric])
    1.33 +    by (simp add:var_same)
    1.34    with ih2 have "elim [(v, N)] v" by blast
    1.35    hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
    1.36    hence not_in_N: "v \<notin> vars_of N" by simp