changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
authorkrauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 4436774c08021ab2e
parent 44361 75ec83d45303
child 44368 91e8062605d5
changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/ROOT.ML
src/HOL/Subst/AList.thy
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sun Aug 21 11:03:15 2011 -0700
     1.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sun Aug 21 22:13:04 2011 +0200
     1.3 @@ -28,11 +28,12 @@
     1.4    TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
     1.5    LET             > HOL4Compat.LET;
     1.6  
     1.7 -ignore_thms
     1.8 +(*ignore_thms
     1.9    BOUNDED_DEF
    1.10    BOUNDED_THM
    1.11    UNBOUNDED_DEF
    1.12    UNBOUNDED_THM;
    1.13 +*)
    1.14  
    1.15  end_import;
    1.16  
     2.1 --- a/src/HOL/Import/Generate-HOL/ROOT.ML	Sun Aug 21 11:03:15 2011 -0700
     2.2 +++ b/src/HOL/Import/Generate-HOL/ROOT.ML	Sun Aug 21 22:13:04 2011 +0200
     2.3 @@ -1,3 +1,5 @@
     2.4 +Runtime.debug := true;
     2.5 +
     2.6  use_thy "GenHOL4Prob";
     2.7  use_thy "GenHOL4Vec";
     2.8  use_thy "GenHOL4Word32";
     3.1 --- a/src/HOL/Subst/AList.thy	Sun Aug 21 11:03:15 2011 -0700
     3.2 +++ b/src/HOL/Subst/AList.thy	Sun Aug 21 22:13:04 2011 +0200
     3.3 @@ -23,4 +23,6 @@
     3.4      "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
     3.5    by (induct l) auto
     3.6  
     3.7 +
     3.8 +
     3.9  end
     4.1 --- a/src/HOL/ex/Unification.thy	Sun Aug 21 11:03:15 2011 -0700
     4.2 +++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4  datatype 'a trm = 
     4.5    Var 'a 
     4.6    | Const 'a
     4.7 -  | App "'a trm" "'a trm" (infix "\<cdot>" 60)
     4.8 +  | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
     4.9  
    4.10  type_synonym 'a subst = "('a \<times> 'a trm) list"
    4.11  
    4.12 @@ -42,38 +42,38 @@
    4.13  
    4.14  text {* Applying a substitution to a term: *}
    4.15  
    4.16 -fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
    4.17 +primrec subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<lhd>" 55)
    4.18  where
    4.19 -  "(Var v) \<triangleleft> s = assoc v (Var v) s"
    4.20 -| "(Const c) \<triangleleft> s = (Const c)"
    4.21 -| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
    4.22 +  "(Var v) \<lhd> s = assoc v (Var v) s"
    4.23 +| "(Const c) \<lhd> s = (Const c)"
    4.24 +| "(M \<cdot> N) \<lhd> s = (M \<lhd> s) \<cdot> (N \<lhd> s)"
    4.25  
    4.26  text {* Composition of substitutions: *}
    4.27  
    4.28  fun
    4.29 -  "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
    4.30 +  comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
    4.31  where
    4.32 -  "[] \<bullet> bl = bl"
    4.33 -| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
    4.34 +  "[] \<lozenge> bl = bl"
    4.35 +| "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
    4.36  
    4.37  text {* Equivalence of substitutions: *}
    4.38  
    4.39 -definition eqv (infix "=\<^sub>s" 50)
    4.40 +definition subst_eq (infixr "\<doteq>" 52)
    4.41  where
    4.42 -  "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
    4.43 +  "s1 \<doteq> s2 \<equiv> \<forall>t. t \<lhd> s1 = t \<lhd> s2" 
    4.44  
    4.45  
    4.46  subsection {* Basic lemmas *}
    4.47  
    4.48 -lemma apply_empty[simp]: "t \<triangleleft> [] = t"
    4.49 +lemma apply_empty[simp]: "t \<lhd> [] = t"
    4.50  by (induct t) auto
    4.51  
    4.52 -lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
    4.53 +lemma compose_empty[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
    4.54  by (induct \<sigma>) auto
    4.55  
    4.56 -lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
    4.57 +lemma apply_compose[simp]: "t \<lhd> (s1 \<lozenge> s2) = t \<lhd> s1 \<lhd> s2"
    4.58  proof (induct t)
    4.59 -  case App thus ?case by simp
    4.60 +  case Comb thus ?case by simp
    4.61  next 
    4.62    case Const thus ?case by simp
    4.63  next
    4.64 @@ -85,39 +85,39 @@
    4.65    qed
    4.66  qed
    4.67  
    4.68 -lemma eqv_refl[intro]: "s =\<^sub>s s"
    4.69 -  by (auto simp:eqv_def)
    4.70 +lemma eqv_refl[intro]: "s \<doteq> s"
    4.71 +  by (auto simp:subst_eq_def)
    4.72  
    4.73 -lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
    4.74 -  by (auto simp:eqv_def)
    4.75 +lemma eqv_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
    4.76 +  by (auto simp:subst_eq_def)
    4.77  
    4.78 -lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
    4.79 -  by (auto simp:eqv_def)
    4.80 +lemma eqv_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
    4.81 +  by (auto simp:subst_eq_def)
    4.82  
    4.83 -lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
    4.84 -  by (auto simp:eqv_def)
    4.85 +lemma eqv_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
    4.86 +  by (auto simp:subst_eq_def)
    4.87  
    4.88 -lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
    4.89 -  by (auto simp:eqv_def)
    4.90 +lemma eqv_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
    4.91 +  by (auto simp:subst_eq_def)
    4.92  
    4.93 -lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
    4.94 -  by (auto simp:eqv_def)
    4.95 +lemma compose_eqv: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
    4.96 +  by (auto simp:subst_eq_def)
    4.97  
    4.98 -lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
    4.99 +lemma compose_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
   4.100    by auto
   4.101  
   4.102  
   4.103  subsection {* Specification: Most general unifiers *}
   4.104  
   4.105  definition
   4.106 -  "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
   4.107 +  "Unifier \<sigma> t u \<equiv> (t\<lhd>\<sigma> = u\<lhd>\<sigma>)"
   4.108  
   4.109  definition
   4.110    "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
   4.111 -  \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
   4.112 +  \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
   4.113  
   4.114  lemma MGUI[intro]:
   4.115 -  "\<lbrakk>t \<triangleleft> \<sigma> = u \<triangleleft> \<sigma>; \<And>\<theta>. t \<triangleleft> \<theta> = u \<triangleleft> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>\<rbrakk>
   4.116 +  "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
   4.117    \<Longrightarrow> MGU \<sigma> t u"
   4.118    by (simp only:Unifier_def MGU_def, auto)
   4.119  
   4.120 @@ -130,11 +130,11 @@
   4.121  
   4.122  text {* Occurs check: Proper subterm relation *}
   4.123  
   4.124 -fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   4.125 +fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "<:" 54) 
   4.126  where
   4.127 -  "occ u (Var v) = False"
   4.128 -| "occ u (Const c) = False"
   4.129 -| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
   4.130 +  "occs u (Var v) = False"
   4.131 +| "occs u (Const c) = False"
   4.132 +| "occs u (M \<cdot> N) = (u = M \<or> u = N \<or> occs u M \<or> occs u N)"
   4.133  
   4.134  text {* The unification algorithm: *}
   4.135  
   4.136 @@ -143,41 +143,41 @@
   4.137    "unify (Const c) (M \<cdot> N)   = None"
   4.138  | "unify (M \<cdot> N)   (Const c) = None"
   4.139  | "unify (Const c) (Var v)   = Some [(v, Const c)]"
   4.140 -| "unify (M \<cdot> N)   (Var v)   = (if (occ (Var v) (M \<cdot> N)) 
   4.141 +| "unify (M \<cdot> N)   (Var v)   = (if (occs (Var v) (M \<cdot> N)) 
   4.142                                          then None
   4.143                                          else Some [(v, M \<cdot> N)])"
   4.144 -| "unify (Var v)   M         = (if (occ (Var v) M) 
   4.145 +| "unify (Var v)   M         = (if (occs (Var v) M) 
   4.146                                          then None
   4.147                                          else Some [(v, M)])"
   4.148  | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   4.149  | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   4.150                                      None \<Rightarrow> None |
   4.151 -                                    Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
   4.152 +                                    Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
   4.153                                        of None \<Rightarrow> None |
   4.154 -                                         Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   4.155 +                                         Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
   4.156    by pat_completeness auto
   4.157  
   4.158  declare unify.psimps[simp]
   4.159  
   4.160  subsection {* Partial correctness *}
   4.161  
   4.162 -text {* Some lemmas about occ and MGU: *}
   4.163 +text {* Some lemmas about occs and MGU: *}
   4.164  
   4.165 -lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
   4.166 -  \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
   4.167 +lemma subst_no_occs: "\<not>occs (Var v) t \<Longrightarrow> Var v \<noteq> t
   4.168 +  \<Longrightarrow> t \<lhd> [(v,s)] = t"
   4.169  by (induct t) auto
   4.170  
   4.171  lemma MGU_Var[intro]: 
   4.172 -  assumes no_occ: "\<not>occ (Var v) t"
   4.173 +  assumes no_occs: "\<not>occs (Var v) t"
   4.174    shows "MGU [(v,t)] (Var v) t"
   4.175  proof (intro MGUI exI)
   4.176 -  show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
   4.177 -    by (cases "Var v = t", auto simp:subst_no_occ)
   4.178 +  show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using no_occs
   4.179 +    by (cases "Var v = t", auto simp:subst_no_occs)
   4.180  next
   4.181 -  fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>" 
   4.182 -  show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>" 
   4.183 +  fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
   4.184 +  show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
   4.185    proof
   4.186 -    fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th 
   4.187 +    fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
   4.188        by (induct s) auto
   4.189    qed
   4.190  qed
   4.191 @@ -200,42 +200,42 @@
   4.192  
   4.193    then obtain \<theta>1 \<theta>2 
   4.194      where "unify M M' = Some \<theta>1"
   4.195 -    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   4.196 -    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   4.197 +    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   4.198 +    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   4.199      and MGU_inner: "MGU \<theta>1 M M'" 
   4.200 -    and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
   4.201 +    and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   4.202      by (auto split:option.split_asm)
   4.203  
   4.204    show ?case
   4.205    proof
   4.206      from MGU_inner and MGU_outer
   4.207 -    have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1" 
   4.208 -      and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
   4.209 +    have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
   4.210 +      and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
   4.211        unfolding MGU_def Unifier_def
   4.212        by auto
   4.213 -    thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
   4.214 +    thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
   4.215        by simp
   4.216    next
   4.217 -    fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
   4.218 -    hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
   4.219 -      and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
   4.220 +    fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
   4.221 +    hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
   4.222 +      and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
   4.223  
   4.224      with MGU_inner obtain \<delta>
   4.225 -      where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
   4.226 +      where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
   4.227        unfolding MGU_def Unifier_def
   4.228        by auto
   4.229  
   4.230 -    from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
   4.231 +    from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
   4.232        by (simp add:eqv_dest[OF eqv])
   4.233  
   4.234      with MGU_outer obtain \<rho>
   4.235 -      where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
   4.236 +      where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
   4.237        unfolding MGU_def Unifier_def
   4.238        by auto
   4.239      
   4.240 -    have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
   4.241 +    have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
   4.242        by (rule eqv_intro, auto simp:eqv_dest[OF eqv] eqv_dest[OF eqv2])
   4.243 -    thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
   4.244 +    thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   4.245    qed
   4.246  qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   4.247  
   4.248 @@ -256,50 +256,50 @@
   4.249  text {* Elimination of variables by a substitution: *}
   4.250  
   4.251  definition
   4.252 -  "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   4.253 +  "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<lhd> \<sigma>)"
   4.254  
   4.255 -lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   4.256 +lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<lhd> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   4.257    by (auto simp:elim_def)
   4.258  
   4.259 -lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   4.260 +lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
   4.261    by (auto simp:elim_def)
   4.262  
   4.263 -lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   4.264 -  by (auto simp:elim_def eqv_def)
   4.265 +lemma elim_eqv: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   4.266 +  by (auto simp:elim_def subst_eq_def)
   4.267  
   4.268  
   4.269  text {* Replacing a variable by itself yields an identity subtitution: *}
   4.270  
   4.271 -lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
   4.272 +lemma var_self[intro]: "[(v, Var v)] \<doteq> []"
   4.273  proof
   4.274 -  fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
   4.275 +  fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
   4.276      by (induct t) simp_all
   4.277  qed
   4.278  
   4.279 -lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)"
   4.280 +lemma var_same: "([(v, t)] \<doteq> []) = (t = Var v)"
   4.281  proof
   4.282    assume t_v: "t = Var v"
   4.283 -  thus "[(v, t)] =\<^sub>s []"
   4.284 +  thus "[(v, t)] \<doteq> []"
   4.285      by auto
   4.286  next
   4.287 -  assume id: "[(v, t)] =\<^sub>s []"
   4.288 +  assume id: "[(v, t)] \<doteq> []"
   4.289    show "t = Var v"
   4.290    proof -
   4.291 -    have "t = Var v \<triangleleft> [(v, t)]" by simp
   4.292 -    also from id have "\<dots> = Var v \<triangleleft> []" ..
   4.293 +    have "t = Var v \<lhd> [(v, t)]" by simp
   4.294 +    also from id have "\<dots> = Var v \<lhd> []" ..
   4.295      finally show ?thesis by simp
   4.296    qed
   4.297  qed
   4.298  
   4.299 -text {* A lemma about occ and elim *}
   4.300 +text {* A lemma about occs and elim *}
   4.301  
   4.302  lemma remove_var:
   4.303    assumes [simp]: "v \<notin> vars_of s"
   4.304 -  shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
   4.305 +  shows "v \<notin> vars_of (t \<lhd> [(v, s)])"
   4.306    by (induct t) simp_all
   4.307  
   4.308 -lemma occ_elim: "\<not>occ (Var v) t 
   4.309 -  \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
   4.310 +lemma occs_elim: "\<not>occs (Var v) t 
   4.311 +  \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
   4.312  proof (induct t)
   4.313    case (Var x)
   4.314    show ?case
   4.315 @@ -319,29 +319,29 @@
   4.316      by (auto intro!:remove_var)
   4.317    thus ?case ..
   4.318  next
   4.319 -  case (App M N)
   4.320 +  case (Comb M N)
   4.321    
   4.322 -  hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
   4.323 -    and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
   4.324 -    and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
   4.325 +  hence ih1: "elim [(v, M)] v \<or> [(v, M)] \<doteq> []"
   4.326 +    and ih2: "elim [(v, N)] v \<or> [(v, N)] \<doteq> []"
   4.327 +    and nonoccs: "Var v \<noteq> M" "Var v \<noteq> N"
   4.328      by auto
   4.329  
   4.330 -  from nonocc have "\<not> [(v,M)] =\<^sub>s []"
   4.331 +  from nonoccs have "\<not> [(v,M)] \<doteq> []"
   4.332      by (simp add:var_same)
   4.333    with ih1 have "elim [(v, M)] v" by blast
   4.334 -  hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
   4.335 +  hence "v \<notin> vars_of (Var v \<lhd> [(v,M)])" ..
   4.336    hence not_in_M: "v \<notin> vars_of M" by simp
   4.337  
   4.338 -  from nonocc have "\<not> [(v,N)] =\<^sub>s []"
   4.339 +  from nonoccs have "\<not> [(v,N)] \<doteq> []"
   4.340      by (simp add:var_same)
   4.341    with ih2 have "elim [(v, N)] v" by blast
   4.342 -  hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
   4.343 +  hence "v \<notin> vars_of (Var v \<lhd> [(v,N)])" ..
   4.344    hence not_in_N: "v \<notin> vars_of N" by simp
   4.345  
   4.346    have "elim [(v, M \<cdot> N)] v"
   4.347    proof 
   4.348      fix t 
   4.349 -    show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
   4.350 +    show "v \<notin> vars_of (t \<lhd> [(v, M \<cdot> N)])"
   4.351      proof (induct t)
   4.352        case (Var x) thus ?case by (simp add: not_in_M not_in_N)
   4.353      qed auto
   4.354 @@ -354,7 +354,7 @@
   4.355  lemma unify_vars: 
   4.356    assumes "unify_dom (M, N)"
   4.357    assumes "unify M N = Some \<sigma>"
   4.358 -  shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   4.359 +  shows "vars_of (t \<lhd> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   4.360    (is "?P M N \<sigma> t")
   4.361  using assms
   4.362  proof (induct M N arbitrary:\<sigma> t)
   4.363 @@ -363,45 +363,45 @@
   4.364    thus ?case by (induct t) auto
   4.365  next
   4.366    case (4 M N v) 
   4.367 -  hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   4.368 +  hence "\<not>occs (Var v) (M\<cdot>N)" by (cases "occs (Var v) (M\<cdot>N)", auto)
   4.369    with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   4.370    thus ?case by (induct t) auto
   4.371  next
   4.372    case (5 v M)
   4.373 -  hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   4.374 +  hence "\<not>occs (Var v) M" by (cases "occs (Var v) M", auto)
   4.375    with 5 have "\<sigma> = [(v, M)]" by simp
   4.376    thus ?case by (induct t) auto
   4.377  next
   4.378    case (7 M N M' N' \<sigma>)
   4.379    then obtain \<theta>1 \<theta>2 
   4.380      where "unify M M' = Some \<theta>1"
   4.381 -    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   4.382 -    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   4.383 +    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   4.384 +    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   4.385      and ih1: "\<And>t. ?P M M' \<theta>1 t"
   4.386 -    and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
   4.387 +    and ih2: "\<And>t. ?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2 t"
   4.388      by (auto split:option.split_asm)
   4.389  
   4.390    show ?case
   4.391    proof
   4.392 -    fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
   4.393 +    fix v assume a: "v \<in> vars_of (t \<lhd> \<sigma>)"
   4.394      
   4.395      show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   4.396      proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   4.397          \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   4.398        case True
   4.399 -      with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   4.400 +      with ih1 have l:"\<And>t. v \<in> vars_of (t \<lhd> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   4.401          by auto
   4.402        
   4.403 -      from a and ih2[where t="t \<triangleleft> \<theta>1"]
   4.404 -      have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1) 
   4.405 -        \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
   4.406 +      from a and ih2[where t="t \<lhd> \<theta>1"]
   4.407 +      have "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1) 
   4.408 +        \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
   4.409          by auto
   4.410        hence "v \<in> vars_of t"
   4.411        proof
   4.412 -        assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   4.413 +        assume "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
   4.414          with True show ?thesis by (auto dest:l)
   4.415        next
   4.416 -        assume "v \<in> vars_of (t \<triangleleft> \<theta>1)" 
   4.417 +        assume "v \<in> vars_of (t \<lhd> \<theta>1)" 
   4.418          thus ?thesis by (rule l)
   4.419        qed
   4.420        
   4.421 @@ -417,7 +417,7 @@
   4.422  lemma unify_eliminates: 
   4.423    assumes "unify_dom (M, N)"
   4.424    assumes "unify M N = Some \<sigma>"
   4.425 -  shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
   4.426 +  shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> \<doteq> []"
   4.427    (is "?P M N \<sigma>")
   4.428  using assms
   4.429  proof (induct M N arbitrary:\<sigma>)
   4.430 @@ -426,21 +426,21 @@
   4.431    case 2 thus ?case by simp
   4.432  next
   4.433    case (3 c v)
   4.434 -  have no_occ: "\<not> occ (Var v) (Const c)" by simp
   4.435 +  have no_occs: "\<not> occs (Var v) (Const c)" by simp
   4.436    with 3 have "\<sigma> = [(v, Const c)]" by simp
   4.437 -  with occ_elim[OF no_occ]
   4.438 +  with occs_elim[OF no_occs]
   4.439    show ?case by auto
   4.440  next
   4.441    case (4 M N v)
   4.442 -  hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   4.443 +  hence no_occs: "\<not>occs (Var v) (M\<cdot>N)" by (cases "occs (Var v) (M\<cdot>N)", auto)
   4.444    with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   4.445 -  with occ_elim[OF no_occ]
   4.446 +  with occs_elim[OF no_occs]
   4.447    show ?case by auto 
   4.448  next
   4.449    case (5 v M) 
   4.450 -  hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   4.451 +  hence no_occs: "\<not>occs (Var v) M" by (cases "occs (Var v) M", auto)
   4.452    with 5 have "\<sigma> = [(v, M)]" by simp
   4.453 -  with occ_elim[OF no_occ]
   4.454 +  with occs_elim[OF no_occs]
   4.455    show ?case by auto 
   4.456  next 
   4.457    case (6 c d) thus ?case
   4.458 @@ -449,43 +449,43 @@
   4.459    case (7 M N M' N' \<sigma>)
   4.460    then obtain \<theta>1 \<theta>2 
   4.461      where "unify M M' = Some \<theta>1"
   4.462 -    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   4.463 -    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   4.464 +    and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   4.465 +    and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   4.466      and ih1: "?P M M' \<theta>1"
   4.467 -    and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
   4.468 +    and ih2: "?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2"
   4.469      by (auto split:option.split_asm)
   4.470  
   4.471    from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   4.472    have "unify_dom (M, M')"
   4.473      by (rule accp_downward) (rule unify_rel.intros)
   4.474    hence no_new_vars: 
   4.475 -    "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   4.476 +    "\<And>t. vars_of (t \<lhd> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   4.477      by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
   4.478  
   4.479    from ih2 show ?case 
   4.480    proof 
   4.481 -    assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
   4.482 +    assume "\<exists>v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1). elim \<theta>2 v"
   4.483      then obtain v 
   4.484 -      where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   4.485 +      where "v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
   4.486        and el: "elim \<theta>2 v" by auto
   4.487      with no_new_vars show ?thesis unfolding \<sigma> 
   4.488        by (auto simp:elim_def)
   4.489    next
   4.490 -    assume empty[simp]: "\<theta>2 =\<^sub>s []"
   4.491 +    assume empty[simp]: "\<theta>2 \<doteq> []"
   4.492  
   4.493 -    have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
   4.494 +    have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
   4.495        by (rule compose_eqv) auto
   4.496 -    also have "\<dots> =\<^sub>s \<theta>1" by auto
   4.497 -    finally have "\<sigma> =\<^sub>s \<theta>1" .
   4.498 +    also have "\<dots> \<doteq> \<theta>1" by auto
   4.499 +    finally have "\<sigma> \<doteq> \<theta>1" .
   4.500  
   4.501      from ih1 show ?thesis
   4.502      proof
   4.503        assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   4.504 -      with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
   4.505 +      with elim_eqv[OF `\<sigma> \<doteq> \<theta>1`]
   4.506        show ?thesis by auto
   4.507      next
   4.508 -      note `\<sigma> =\<^sub>s \<theta>1`
   4.509 -      also assume "\<theta>1 =\<^sub>s []"
   4.510 +      note `\<sigma> \<doteq> \<theta>1`
   4.511 +      also assume "\<theta>1 \<doteq> []"
   4.512        finally show ?thesis ..
   4.513      qed
   4.514    qed
   4.515 @@ -509,7 +509,7 @@
   4.516      "unify M M' = Some \<theta>"
   4.517  
   4.518    from unify_eliminates[OF inner]
   4.519 -  show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   4.520 +  show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   4.521    proof
   4.522      -- {* Either a variable is eliminated \ldots *}
   4.523      assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   4.524 @@ -517,7 +517,7 @@
   4.525        where "elim \<theta> v" 
   4.526        and "v\<in>vars_of M \<union> vars_of M'" by auto
   4.527      with unify_vars[OF inner]
   4.528 -    have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
   4.529 +    have "vars_of (N\<lhd>\<theta>) \<union> vars_of (N'\<lhd>\<theta>)
   4.530        \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   4.531        by auto
   4.532      
   4.533 @@ -525,9 +525,9 @@
   4.534        by (auto intro!: measures_less intro: psubset_card_mono)
   4.535    next
   4.536      -- {* Or the substitution is empty *}
   4.537 -    assume "\<theta> =\<^sub>s []"
   4.538 -    hence "N \<triangleleft> \<theta> = N" 
   4.539 -      and "N' \<triangleleft> \<theta> = N'" by auto
   4.540 +    assume "\<theta> \<doteq> []"
   4.541 +    hence "N \<lhd> \<theta> = N" 
   4.542 +      and "N' \<lhd> \<theta> = N'" by auto
   4.543      thus ?thesis 
   4.544         by (auto intro!: measures_less intro: psubset_card_mono)
   4.545    qed