author krauss Sun Aug 21 22:13:04 2011 +0200 (2011-08-21) changeset 44369 02e13192a053 parent 44368 91e8062605d5 child 44370 03d91bfad83b
tuned notation
```     1.1 --- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
1.2 +++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
1.3 @@ -41,9 +41,9 @@
1.4
1.5  fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54)
1.6  where
1.7 -  "occs u (Var v) = False"
1.8 -| "occs u (Const c) = False"
1.9 -| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
1.10 +  "u \<prec> Var v \<longleftrightarrow> False"
1.11 +| "u \<prec> Const c \<longleftrightarrow> False"
1.12 +| "u \<prec> M \<cdot> N \<longleftrightarrow> u = M \<or> u = N \<or> u \<prec> M \<or> u \<prec> N"
1.13
1.14
1.15  lemma finite_vars_of[intro]: "finite (vars_of t)"
1.16 @@ -175,10 +175,10 @@
1.17    "unify (Const c) (M \<cdot> N)   = None"
1.18  | "unify (M \<cdot> N)   (Const c) = None"
1.19  | "unify (Const c) (Var v)   = Some [(v, Const c)]"
1.20 -| "unify (M \<cdot> N)   (Var v)   = (if (occs (Var v) (M \<cdot> N))
1.21 +| "unify (M \<cdot> N)   (Var v)   = (if Var v \<prec> M \<cdot> N
1.22                                          then None
1.23                                          else Some [(v, M \<cdot> N)])"
1.24 -| "unify (Var v)   M         = (if (occs (Var v) M)
1.25 +| "unify (Var v)   M         = (if Var v \<prec> M
1.26                                          then None
1.27                                          else Some [(v, M)])"
1.28  | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
1.29 @@ -195,12 +195,12 @@
1.30
1.31  text {* Some lemmas about occs and MGU: *}
1.32
1.33 -lemma subst_no_occs: "\<not>occs (Var v) t \<Longrightarrow> Var v \<noteq> t
1.34 +lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
1.35    \<Longrightarrow> t \<lhd> [(v,s)] = t"
1.36  by (induct t) auto
1.37
1.38  lemma MGU_Var[intro]:
1.39 -  assumes no_occs: "\<not>occs (Var v) t"
1.40 +  assumes no_occs: "\<not> Var v \<prec> t"
1.41    shows "MGU [(v,t)] (Var v) t"
1.42  proof (intro MGUI exI)
1.43    show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using no_occs
1.44 @@ -320,7 +320,7 @@
1.45    shows "v \<notin> vars_of (t \<lhd> [(v, s)])"
1.46    by (induct t) simp_all
1.47
1.48 -lemma occs_elim: "\<not>occs (Var v) t
1.49 +lemma occs_elim: "\<not> Var v \<prec> t
1.50    \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
1.51  proof (induct t)
1.52    case (Var x)
1.53 @@ -385,12 +385,12 @@
1.54    thus ?case by (induct t) auto
1.55  next
1.56    case (4 M N v)
1.57 -  hence "\<not>occs (Var v) (M\<cdot>N)" by (cases "occs (Var v) (M\<cdot>N)", auto)
1.58 +  hence "\<not> Var v \<prec> M \<cdot> N" by auto
1.59    with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
1.60    thus ?case by (induct t) auto
1.61  next
1.62    case (5 v M)
1.63 -  hence "\<not>occs (Var v) M" by (cases "occs (Var v) M", auto)
1.64 +  hence "\<not> Var v \<prec> M" by auto
1.65    with 5 have "\<sigma> = [(v, M)]" by simp
1.66    thus ?case by (induct t) auto
1.67  next
1.68 @@ -448,19 +448,19 @@
1.69    case 2 thus ?case by simp
1.70  next
1.71    case (3 c v)
1.72 -  have no_occs: "\<not> occs (Var v) (Const c)" by simp
1.73 +  have no_occs: "\<not> Var v \<prec> Const c" by simp
1.74    with 3 have "\<sigma> = [(v, Const c)]" by simp
1.75    with occs_elim[OF no_occs]
1.76    show ?case by auto
1.77  next
1.78    case (4 M N v)
1.79 -  hence no_occs: "\<not>occs (Var v) (M\<cdot>N)" by (cases "occs (Var v) (M\<cdot>N)", auto)
1.80 +  hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
1.81    with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
1.82    with occs_elim[OF no_occs]
1.83    show ?case by auto
1.84  next
1.85    case (5 v M)
1.86 -  hence no_occs: "\<not>occs (Var v) M" by (cases "occs (Var v) M", auto)
1.87 +  hence no_occs: "\<not> Var v \<prec> M" by auto
1.88    with 5 have "\<sigma> = [(v, M)]" by simp
1.89    with occs_elim[OF no_occs]
1.90    show ?case by auto
```