--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Unification.thy Thu May 17 22:33:41 2007 +0200
@@ -0,0 +1,554 @@
+(* ID: $Id$
+ Author: Alexander Krauss, Technische Universitaet Muenchen
+*)
+
+header {* Case study: Unification Algorithm *}
+
+(*<*)theory Unification
+imports Main
+begin(*>*)
+
+text {*
+ This is a formalization of a first-order unification
+ algorithm. It uses the new "function" package to define recursive
+ functions, which allows a better treatment of nested recursion.
+
+ This is basically a modernized version of a previous formalization
+ by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
+ previous work by Paulson and Manna & Waldinger (for details, see
+ there).
+
+ Unlike that formalization, where the proofs of termination and
+ some partial correctness properties are intertwined, we can prove
+ partial correctness and termination separately.
+*}
+
+subsection {* Basic definitions *}
+
+datatype 'a trm =
+ Var 'a
+ | Const 'a
+ | App "'a trm" "'a trm" (infix "\<cdot>" 60)
+
+types
+ 'a subst = "('a \<times> 'a trm) list"
+
+text {* Applying a substitution to a variable: *}
+
+fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
+where
+ "assoc x d [] = d"
+| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
+
+text {* Applying a substitution to a term: *}
+
+fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
+where
+ "(Var v) \<triangleleft> s = assoc v (Var v) s"
+| "(Const c) \<triangleleft> s = (Const c)"
+| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
+
+text {* Composition of substitutions: *}
+
+fun
+ "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
+where
+ "[] \<bullet> bl = bl"
+| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
+
+text {* Equivalence of substitutions: *}
+
+definition eqv (infix "=\<^sub>s" 50)
+where
+ "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
+
+subsection {* Basic lemmas *}
+
+lemma apply_empty[simp]: "t \<triangleleft> [] = t"
+by (induct t) auto
+
+lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
+by (induct \<sigma>) auto
+
+lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
+proof (induct t)
+ case App thus ?case by simp
+next
+ case Const thus ?case by simp
+next
+ case (Var v) thus ?case
+ proof (induct s1)
+ case Nil show ?case by simp
+ next
+ case (Cons p s1s) thus ?case by (cases p, simp)
+ qed
+qed
+
+lemma eqv_refl[intro]: "s =\<^sub>s s"
+ by (auto simp:eqv_def)
+
+lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
+ by (auto simp:eqv_def)
+
+lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
+ by (auto simp:eqv_def)
+
+lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
+ by (auto simp:eqv_def)
+
+lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
+ by (auto simp:eqv_def)
+
+lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
+ by (auto simp:eqv_def)
+
+lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
+ by auto
+
+subsection {* Specification: Most general unifiers *}
+
+definition
+ "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
+
+definition
+ "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u
+ \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
+
+lemma MGUI[intro]:
+ "\<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>
+ \<Longrightarrow> MGU \<sigma> t u"
+ by (simp only:Unifier_def MGU_def, auto)
+
+lemma MGU_sym[sym]:
+ "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
+ by (auto simp:MGU_def Unifier_def)
+
+
+subsection {* The unification algorithm *}
+
+text {* Occurs check: Proper subterm relation *}
+
+fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
+where
+ "occ u (Var v) = False"
+| "occ u (Const c) = False"
+| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
+
+text {* The unification algorithm: *}
+
+function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
+where
+ "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 (occ (Var v) (M \<cdot> N))
+ then None
+ else Some [(v, M \<cdot> N)])"
+| "unify (Var v) M = (if (occ (Var v) M)
+ then None
+ else Some [(v, M)])"
+| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
+| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
+ None \<Rightarrow> None |
+ Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
+ of None \<Rightarrow> None |
+ Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
+ by pat_completeness auto
+
+
+subsection {* Partial correctness *}
+
+text {* Some lemmas about occ and MGU: *}
+
+lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
+ \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
+by (induct t) auto
+
+lemma MGU_Var[intro]:
+ assumes no_occ: "\<not>occ (Var v) t"
+ shows "MGU [(v,t)] (Var v) t"
+proof (intro MGUI exI)
+ show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
+ by (cases "Var v = t", auto simp:subst_no_occ)
+next
+ fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
+ show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
+ proof
+ fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
+ by (induct s, auto)
+ qed
+qed
+
+declare MGU_Var[symmetric, intro]
+
+lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
+ unfolding MGU_def Unifier_def
+ by auto
+
+text {* If unification terminates, then it computes most general unifiers: *}
+
+lemma unify_partial_correctness:
+ assumes "unify_dom (M, N)"
+ assumes "unify M N = Some \<sigma>"
+ shows "MGU \<sigma> M N"
+using prems
+proof (induct M N arbitrary: \<sigma>)
+ case (7 M N M' N' \<sigma>) -- "The interesting case"
+
+ then obtain \<theta>1 \<theta>2
+ where "unify M M' = Some \<theta>1"
+ and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
+ and MGU_inner: "MGU \<theta>1 M M'"
+ and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
+ by (auto split:option.split_asm)
+
+ show ?case
+ proof
+ from MGU_inner and MGU_outer
+ have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1"
+ and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
+ unfolding MGU_def Unifier_def
+ by auto
+ thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
+ by simp
+ next
+ fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
+ hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
+ and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
+
+ with MGU_inner obtain \<delta>
+ where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
+ unfolding MGU_def Unifier_def
+ by auto
+
+ from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
+ by (simp add:eqv_dest[OF eqv])
+
+ with MGU_outer obtain \<rho>
+ where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
+ unfolding MGU_def Unifier_def
+ by auto
+
+ have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
+ by (rule eqv_intro, auto simp:eqv_dest[OF eqv]
+ eqv_dest[OF eqv2])
+ thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
+ qed
+qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
+
+
+subsection {* Properties used in termination proof *}
+
+text {* The variables of a term: *}
+
+fun vars_of:: "'a trm \<Rightarrow> 'a set"
+where
+ "vars_of (Var v) = { v }"
+| "vars_of (Const c) = {}"
+| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
+
+lemma vars_of_finite[intro]: "finite (vars_of t)"
+ by (induct t) simp_all
+
+text {* Elimination of variables by a substitution: *}
+
+definition
+ "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
+
+lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
+ by (auto simp:elim_def)
+
+lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
+ by (auto simp:elim_def)
+
+lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
+ by (auto simp:elim_def eqv_def)
+
+
+text {* Replacing a variable by itself yields an identity subtitution: *}
+
+lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
+proof
+ fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
+ by (induct t) simp_all
+qed
+
+lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
+proof
+ assume t_v: "t = Var v"
+ thus "[(v, t)] =\<^sub>s []"
+ by auto
+next
+ assume id: "[(v, t)] =\<^sub>s []"
+ show "t = Var v"
+ proof -
+ have "t = Var v \<triangleleft> [(v, t)]" by simp
+ also from id have "\<dots> = Var v \<triangleleft> []" ..
+ finally show ?thesis by simp
+ qed
+qed
+
+text {* A lemma about occ and elim *}
+
+lemma remove_var:
+ assumes [simp]: "v \<notin> vars_of s"
+ shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
+ by (induct t) simp_all
+
+lemma occ_elim: "\<not>occ (Var v) t
+ \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
+proof (induct t)
+ case (Var x)
+ show ?case
+ proof cases
+ assume "v = x"
+ thus ?thesis
+ by (simp add:var_same[symmetric])
+ next
+ assume neq: "v \<noteq> x"
+ have "elim [(v, Var x)] v"
+ by (auto intro!:remove_var simp:neq)
+ thus ?thesis ..
+ qed
+next
+ case (Const c)
+ have "elim [(v, Const c)] v"
+ by (auto intro!:remove_var)
+ thus ?case ..
+next
+ case (App M N)
+
+ hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
+ and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
+ and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
+ by auto
+
+ from nonocc have "\<not> [(v,M)] =\<^sub>s []"
+ by (simp add:var_same[symmetric])
+ with ih1 have "elim [(v, M)] v" by blast
+ hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
+ hence not_in_M: "v \<notin> vars_of M" by simp
+
+ from nonocc have "\<not> [(v,N)] =\<^sub>s []"
+ by (simp add:var_same[symmetric])
+ with ih2 have "elim [(v, N)] v" by blast
+ hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
+ hence not_in_N: "v \<notin> vars_of N" by simp
+
+ have "elim [(v, M \<cdot> N)] v"
+ proof
+ fix t
+ show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
+ proof (induct t)
+ case (Var x) thus ?case by (simp add: not_in_M not_in_N)
+ qed auto
+ qed
+ thus ?case ..
+qed
+
+text {* The result of a unification never introduces new variables: *}
+
+lemma unify_vars:
+ assumes "unify_dom (M, N)"
+ assumes "unify M N = Some \<sigma>"
+ shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
+ (is "?P M N \<sigma> t")
+using prems
+proof (induct M N arbitrary:\<sigma> t)
+ case (3 c v)
+ hence "\<sigma> = [(v, Const c)]" by simp
+ thus ?case by (induct t, auto)
+next
+ case (4 M N v)
+ hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
+ with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
+ thus ?case by (induct t, auto)
+next
+ case (5 v M)
+ hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
+ with prems have "\<sigma> = [(v, M)]" by simp
+ thus ?case by (induct t, auto)
+next
+ case (7 M N M' N' \<sigma>)
+ then obtain \<theta>1 \<theta>2
+ where "unify M M' = Some \<theta>1"
+ and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
+ and ih1: "\<And>t. ?P M M' \<theta>1 t"
+ and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
+ by (auto split:option.split_asm)
+
+ show ?case
+ proof
+ fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
+
+ show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
+ proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
+ \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
+ case True
+ with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
+ by auto
+
+ from a and ih2[where t="t \<triangleleft> \<theta>1"]
+ have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)
+ \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
+ by auto
+ hence "v \<in> vars_of t"
+ proof
+ assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
+ with True show ?thesis by (auto dest:l)
+ next
+ assume "v \<in> vars_of (t \<triangleleft> \<theta>1)"
+ thus ?thesis by (rule l)
+ qed
+
+ thus ?thesis by auto
+ qed auto
+ qed
+qed (auto split: split_if_asm)
+
+
+text {* The result of a unification is either the identity
+substitution or it eliminates a variable from one of the terms: *}
+
+lemma unify_eliminates:
+ assumes "unify_dom (M, N)"
+ assumes "unify M N = Some \<sigma>"
+ shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
+ (is "?P M N \<sigma>")
+using prems
+proof (induct M N arbitrary:\<sigma>)
+ case 1 thus ?case by simp
+next
+ case 2 thus ?case by simp
+next
+ case (3 c v)
+ have no_occ: "\<not> occ (Var v) (Const c)" by simp
+ with prems have "\<sigma> = [(v, Const c)]" by simp
+ with occ_elim[OF no_occ]
+ show ?case by auto
+next
+ case (4 M N v)
+ hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
+ with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
+ with occ_elim[OF no_occ]
+ show ?case by auto
+next
+ case (5 v M)
+ hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
+ with prems have "\<sigma> = [(v, M)]" by simp
+ with occ_elim[OF no_occ]
+ show ?case by auto
+next
+ case (6 c d) thus ?case
+ by (cases "c = d") auto
+next
+ case (7 M N M' N' \<sigma>)
+ then obtain \<theta>1 \<theta>2
+ where "unify M M' = Some \<theta>1"
+ and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
+ and ih1: "?P M M' \<theta>1"
+ and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
+ by (auto split:option.split_asm)
+
+ from `unify_dom (M \<cdot> N, M' \<cdot> N')`
+ have "unify_dom (M, M')"
+ by (rule acc_downward) (rule unify_rel.intros)
+ hence no_new_vars:
+ "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
+ by (rule unify_vars)
+
+ from ih2 show ?case
+ proof
+ assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
+ then obtain v
+ where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
+ and el: "elim \<theta>2 v" by auto
+ with no_new_vars show ?thesis unfolding \<sigma>
+ by (auto simp:elim_def)
+ next
+ assume empty[simp]: "\<theta>2 =\<^sub>s []"
+
+ have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
+ by (rule compose_eqv) auto
+ also have "\<dots> =\<^sub>s \<theta>1" by auto
+ finally have "\<sigma> =\<^sub>s \<theta>1" .
+
+ from ih1 show ?thesis
+ proof
+ assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
+ with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
+ show ?thesis by auto
+ next
+ note `\<sigma> =\<^sub>s \<theta>1`
+ also assume "\<theta>1 =\<^sub>s []"
+ finally show ?thesis ..
+ qed
+ qed
+qed
+
+
+subsection {* Termination proof *}
+
+
+termination unify
+proof
+ let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
+ \<lambda>(M, N). size M]"
+ show "wf ?R" by simp
+
+ fix M N M' N'
+ show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
+ by (rule measures_lesseq) (auto intro: card_mono)
+
+ fix \<theta> -- "Outer call"
+ assume inner: "unify_dom (M, M')"
+ "unify M M' = Some \<theta>"
+
+ from unify_eliminates[OF inner]
+ show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
+ proof
+ -- {* Either a variable is eliminated \ldots *}
+ assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
+ then obtain v
+ where "elim \<theta> v"
+ and "v\<in>vars_of M \<union> vars_of M'" by auto
+ with unify_vars[OF inner]
+ have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
+ \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
+ by auto
+
+ thus ?thesis
+ by (auto intro!: measures_less intro: psubset_card_mono)
+ next
+ -- {* Or the substitution is empty *}
+ assume "\<theta> =\<^sub>s []"
+ hence "N \<triangleleft> \<theta> = N"
+ and "N' \<triangleleft> \<theta> = N'" by auto
+ thus ?thesis
+ by (auto intro!: measures_less intro: psubset_card_mono)
+ qed
+qed
+
+
+(*<*)end(*>*)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+