# HG changeset patch
# User krauss
# Date 1313957584 -7200
# Node ID 02e13192a053048f2b321296ece5199c48e17cc0
# Parent  91e8062605d575b864299309cd2c9e90b1650c6c
tuned notation

diff -r 91e8062605d5 -r 02e13192a053 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -41,9 +41,9 @@
 
 fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54) 
 where
-  "occs u (Var v) = False"
-| "occs u (Const c) = False"
-| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
+  "u \<prec> Var v \<longleftrightarrow> False"
+| "u \<prec> Const c \<longleftrightarrow> False"
+| "u \<prec> M \<cdot> N \<longleftrightarrow> u = M \<or> u = N \<or> u \<prec> M \<or> u \<prec> N"
 
 
 lemma finite_vars_of[intro]: "finite (vars_of t)"
@@ -175,10 +175,10 @@
   "unify (Const c) (M \<cdot> N)   = None"
 | "unify (M \<cdot> N)   (Const c) = None"
 | "unify (Const c) (Var v)   = Some [(v, Const c)]"
-| "unify (M \<cdot> N)   (Var v)   = (if (occs (Var v) (M \<cdot> N)) 
+| "unify (M \<cdot> N)   (Var v)   = (if Var v \<prec> M \<cdot> N 
                                         then None
                                         else Some [(v, M \<cdot> N)])"
-| "unify (Var v)   M         = (if (occs (Var v) M) 
+| "unify (Var v)   M         = (if Var v \<prec> M
                                         then None
                                         else Some [(v, M)])"
 | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
@@ -195,12 +195,12 @@
 
 text {* Some lemmas about occs and MGU: *}
 
-lemma subst_no_occs: "\<not>occs (Var v) t \<Longrightarrow> Var v \<noteq> t
+lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
   \<Longrightarrow> t \<lhd> [(v,s)] = t"
 by (induct t) auto
 
 lemma MGU_Var[intro]: 
-  assumes no_occs: "\<not>occs (Var v) t"
+  assumes no_occs: "\<not> Var v \<prec> t"
   shows "MGU [(v,t)] (Var v) t"
 proof (intro MGUI exI)
   show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using no_occs
@@ -320,7 +320,7 @@
   shows "v \<notin> vars_of (t \<lhd> [(v, s)])"
   by (induct t) simp_all
 
-lemma occs_elim: "\<not>occs (Var v) t 
+lemma occs_elim: "\<not> Var v \<prec> t 
   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
 proof (induct t)
   case (Var x)
@@ -385,12 +385,12 @@
   thus ?case by (induct t) auto
 next
   case (4 M N v) 
-  hence "\<not>occs (Var v) (M\<cdot>N)" by (cases "occs (Var v) (M\<cdot>N)", auto)
+  hence "\<not> Var v \<prec> M \<cdot> N" by auto
   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   thus ?case by (induct t) auto
 next
   case (5 v M)
-  hence "\<not>occs (Var v) M" by (cases "occs (Var v) M", auto)
+  hence "\<not> Var v \<prec> M" by auto
   with 5 have "\<sigma> = [(v, M)]" by simp
   thus ?case by (induct t) auto
 next
@@ -448,19 +448,19 @@
   case 2 thus ?case by simp
 next
   case (3 c v)
-  have no_occs: "\<not> occs (Var v) (Const c)" by simp
+  have no_occs: "\<not> Var v \<prec> Const c" by simp
   with 3 have "\<sigma> = [(v, Const c)]" by simp
   with occs_elim[OF no_occs]
   show ?case by auto
 next
   case (4 M N v)
-  hence no_occs: "\<not>occs (Var v) (M\<cdot>N)" by (cases "occs (Var v) (M\<cdot>N)", auto)
+  hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   with occs_elim[OF no_occs]
   show ?case by auto 
 next
   case (5 v M) 
-  hence no_occs: "\<not>occs (Var v) M" by (cases "occs (Var v) M", auto)
+  hence no_occs: "\<not> Var v \<prec> M" by auto
   with 5 have "\<sigma> = [(v, M)]" by simp
   with occs_elim[OF no_occs]
   show ?case by auto