src/HOL/ex/Unification.thy
changeset 44369 02e13192a053
parent 44368 91e8062605d5
child 44370 03d91bfad83b
     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