src/HOL/ex/Unification.thy
 author wenzelm Tue Aug 28 11:25:29 2007 +0200 (2007-08-28) changeset 24444 448978b61556 parent 23777 60b7800338d5 child 30909 bd4f255837e5 permissions -rw-r--r--
induct: proper separation of initial and terminal step;
avoid unspecific prems;
1 (*  ID:         \$Id\$
2     Author:     Alexander Krauss, Technische Universitaet Muenchen
3 *)
5 header {* Case study: Unification Algorithm *}
7 theory Unification
8 imports Main
9 begin
11 text {*
12   This is a formalization of a first-order unification
13   algorithm. It uses the new "function" package to define recursive
14   functions, which allows a better treatment of nested recursion.
16   This is basically a modernized version of a previous formalization
17   by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
18   previous work by Paulson and Manna \& Waldinger (for details, see
19   there).
21   Unlike that formalization, where the proofs of termination and
22   some partial correctness properties are intertwined, we can prove
23   partial correctness and termination separately.
24 *}
27 subsection {* Basic definitions *}
29 datatype 'a trm =
30   Var 'a
31   | Const 'a
32   | App "'a trm" "'a trm" (infix "\<cdot>" 60)
34 types
35   'a subst = "('a \<times> 'a trm) list"
37 text {* Applying a substitution to a variable: *}
39 fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
40 where
41   "assoc x d [] = d"
42 | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
44 text {* Applying a substitution to a term: *}
46 fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
47 where
48   "(Var v) \<triangleleft> s = assoc v (Var v) s"
49 | "(Const c) \<triangleleft> s = (Const c)"
50 | "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
52 text {* Composition of substitutions: *}
54 fun
55   "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
56 where
57   "[] \<bullet> bl = bl"
58 | "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
60 text {* Equivalence of substitutions: *}
62 definition eqv (infix "=\<^sub>s" 50)
63 where
64   "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
67 subsection {* Basic lemmas *}
69 lemma apply_empty[simp]: "t \<triangleleft> [] = t"
70 by (induct t) auto
72 lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
73 by (induct \<sigma>) auto
75 lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
76 proof (induct t)
77   case App thus ?case by simp
78 next
79   case Const thus ?case by simp
80 next
81   case (Var v) thus ?case
82   proof (induct s1)
83     case Nil show ?case by simp
84   next
85     case (Cons p s1s) thus ?case by (cases p, simp)
86   qed
87 qed
89 lemma eqv_refl[intro]: "s =\<^sub>s s"
90   by (auto simp:eqv_def)
92 lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
93   by (auto simp:eqv_def)
95 lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
96   by (auto simp:eqv_def)
98 lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
99   by (auto simp:eqv_def)
101 lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
102   by (auto simp:eqv_def)
104 lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
105   by (auto simp:eqv_def)
107 lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
108   by auto
111 subsection {* Specification: Most general unifiers *}
113 definition
114   "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
116 definition
117   "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u
118   \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
120 lemma MGUI[intro]:
121   "\<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>
122   \<Longrightarrow> MGU \<sigma> t u"
123   by (simp only:Unifier_def MGU_def, auto)
125 lemma MGU_sym[sym]:
126   "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
127   by (auto simp:MGU_def Unifier_def)
130 subsection {* The unification algorithm *}
132 text {* Occurs check: Proper subterm relation *}
134 fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
135 where
136   "occ u (Var v) = False"
137 | "occ u (Const c) = False"
138 | "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
140 text {* The unification algorithm: *}
142 function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
143 where
144   "unify (Const c) (M \<cdot> N)   = None"
145 | "unify (M \<cdot> N)   (Const c) = None"
146 | "unify (Const c) (Var v)   = Some [(v, Const c)]"
147 | "unify (M \<cdot> N)   (Var v)   = (if (occ (Var v) (M \<cdot> N))
148                                         then None
149                                         else Some [(v, M \<cdot> N)])"
150 | "unify (Var v)   M         = (if (occ (Var v) M)
151                                         then None
152                                         else Some [(v, M)])"
153 | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
154 | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
155                                     None \<Rightarrow> None |
156                                     Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
157                                       of None \<Rightarrow> None |
158                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
159   by pat_completeness auto
162 subsection {* Partial correctness *}
164 text {* Some lemmas about occ and MGU: *}
166 lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
167   \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
168 by (induct t) auto
170 lemma MGU_Var[intro]:
171   assumes no_occ: "\<not>occ (Var v) t"
172   shows "MGU [(v,t)] (Var v) t"
173 proof (intro MGUI exI)
174   show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
175     by (cases "Var v = t", auto simp:subst_no_occ)
176 next
177   fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
178   show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
179   proof
180     fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
181       by (induct s) auto
182   qed
183 qed
185 declare MGU_Var[symmetric, intro]
187 lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
188   unfolding MGU_def Unifier_def
189   by auto
191 text {* If unification terminates, then it computes most general unifiers: *}
193 lemma unify_partial_correctness:
194   assumes "unify_dom (M, N)"
195   assumes "unify M N = Some \<sigma>"
196   shows "MGU \<sigma> M N"
197 using assms
198 proof (induct M N arbitrary: \<sigma>)
199   case (7 M N M' N' \<sigma>) -- "The interesting case"
201   then obtain \<theta>1 \<theta>2
202     where "unify M M' = Some \<theta>1"
203     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
204     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
205     and MGU_inner: "MGU \<theta>1 M M'"
206     and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
207     by (auto split:option.split_asm)
209   show ?case
210   proof
211     from MGU_inner and MGU_outer
212     have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1"
213       and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
214       unfolding MGU_def Unifier_def
215       by auto
216     thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
217       by simp
218   next
219     fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
220     hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
221       and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
223     with MGU_inner obtain \<delta>
224       where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
225       unfolding MGU_def Unifier_def
226       by auto
228     from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
231     with MGU_outer obtain \<rho>
232       where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
233       unfolding MGU_def Unifier_def
234       by auto
236     have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
237       by (rule eqv_intro, auto simp:eqv_dest[OF eqv]
238 	eqv_dest[OF eqv2])
239     thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
240   qed
241 qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
244 subsection {* Properties used in termination proof *}
246 text {* The variables of a term: *}
248 fun vars_of:: "'a trm \<Rightarrow> 'a set"
249 where
250   "vars_of (Var v) = { v }"
251 | "vars_of (Const c) = {}"
252 | "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
254 lemma vars_of_finite[intro]: "finite (vars_of t)"
255   by (induct t) simp_all
257 text {* Elimination of variables by a substitution: *}
259 definition
260   "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
262 lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
263   by (auto simp:elim_def)
265 lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
266   by (auto simp:elim_def)
268 lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
269   by (auto simp:elim_def eqv_def)
272 text {* Replacing a variable by itself yields an identity subtitution: *}
274 lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
275 proof
276   fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
277     by (induct t) simp_all
278 qed
280 lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
281 proof
282   assume t_v: "t = Var v"
283   thus "[(v, t)] =\<^sub>s []"
284     by auto
285 next
286   assume id: "[(v, t)] =\<^sub>s []"
287   show "t = Var v"
288   proof -
289     have "t = Var v \<triangleleft> [(v, t)]" by simp
290     also from id have "\<dots> = Var v \<triangleleft> []" ..
291     finally show ?thesis by simp
292   qed
293 qed
295 text {* A lemma about occ and elim *}
297 lemma remove_var:
298   assumes [simp]: "v \<notin> vars_of s"
299   shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
300   by (induct t) simp_all
302 lemma occ_elim: "\<not>occ (Var v) t
303   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
304 proof (induct t)
305   case (Var x)
306   show ?case
307   proof cases
308     assume "v = x"
309     thus ?thesis
311   next
312     assume neq: "v \<noteq> x"
313     have "elim [(v, Var x)] v"
314       by (auto intro!:remove_var simp:neq)
315     thus ?thesis ..
316   qed
317 next
318   case (Const c)
319   have "elim [(v, Const c)] v"
320     by (auto intro!:remove_var)
321   thus ?case ..
322 next
323   case (App M N)
325   hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
326     and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
327     and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
328     by auto
330   from nonocc have "\<not> [(v,M)] =\<^sub>s []"
332   with ih1 have "elim [(v, M)] v" by blast
333   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
334   hence not_in_M: "v \<notin> vars_of M" by simp
336   from nonocc have "\<not> [(v,N)] =\<^sub>s []"
338   with ih2 have "elim [(v, N)] v" by blast
339   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
340   hence not_in_N: "v \<notin> vars_of N" by simp
342   have "elim [(v, M \<cdot> N)] v"
343   proof
344     fix t
345     show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
346     proof (induct t)
347       case (Var x) thus ?case by (simp add: not_in_M not_in_N)
348     qed auto
349   qed
350   thus ?case ..
351 qed
353 text {* The result of a unification never introduces new variables: *}
355 lemma unify_vars:
356   assumes "unify_dom (M, N)"
357   assumes "unify M N = Some \<sigma>"
358   shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
359   (is "?P M N \<sigma> t")
360 using assms
361 proof (induct M N arbitrary:\<sigma> t)
362   case (3 c v)
363   hence "\<sigma> = [(v, Const c)]" by simp
364   thus ?case by (induct t) auto
365 next
366   case (4 M N v)
367   hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
368   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
369   thus ?case by (induct t) auto
370 next
371   case (5 v M)
372   hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
373   with 5 have "\<sigma> = [(v, M)]" by simp
374   thus ?case by (induct t) auto
375 next
376   case (7 M N M' N' \<sigma>)
377   then obtain \<theta>1 \<theta>2
378     where "unify M M' = Some \<theta>1"
379     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
380     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
381     and ih1: "\<And>t. ?P M M' \<theta>1 t"
382     and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
383     by (auto split:option.split_asm)
385   show ?case
386   proof
387     fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
389     show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
390     proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
391 	    \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
392       case True
393       with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
394 	    by auto
396       from a and ih2[where t="t \<triangleleft> \<theta>1"]
397       have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)
398         \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
399 	    by auto
400       hence "v \<in> vars_of t"
401       proof
402 	    assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
403 	    with True show ?thesis by (auto dest:l)
404       next
405 	    assume "v \<in> vars_of (t \<triangleleft> \<theta>1)"
406 	    thus ?thesis by (rule l)
407       qed
409       thus ?thesis by auto
410     qed auto
411   qed
412 qed (auto split: split_if_asm)
415 text {* The result of a unification is either the identity
416 substitution or it eliminates a variable from one of the terms: *}
418 lemma unify_eliminates:
419   assumes "unify_dom (M, N)"
420   assumes "unify M N = Some \<sigma>"
421   shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
422   (is "?P M N \<sigma>")
423 using assms
424 proof (induct M N arbitrary:\<sigma>)
425   case 1 thus ?case by simp
426 next
427   case 2 thus ?case by simp
428 next
429   case (3 c v)
430   have no_occ: "\<not> occ (Var v) (Const c)" by simp
431   with 3 have "\<sigma> = [(v, Const c)]" by simp
432   with occ_elim[OF no_occ]
433   show ?case by auto
434 next
435   case (4 M N v)
436   hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
437   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
438   with occ_elim[OF no_occ]
439   show ?case by auto
440 next
441   case (5 v M)
442   hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
443   with 5 have "\<sigma> = [(v, M)]" by simp
444   with occ_elim[OF no_occ]
445   show ?case by auto
446 next
447   case (6 c d) thus ?case
448     by (cases "c = d") auto
449 next
450   case (7 M N M' N' \<sigma>)
451   then obtain \<theta>1 \<theta>2
452     where "unify M M' = Some \<theta>1"
453     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
454     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
455     and ih1: "?P M M' \<theta>1"
456     and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
457     by (auto split:option.split_asm)
459   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
460   have "unify_dom (M, M')"
461     by (rule accp_downward) (rule unify_rel.intros)
462   hence no_new_vars:
463     "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
464     by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
466   from ih2 show ?case
467   proof
468     assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
469     then obtain v
470       where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
471       and el: "elim \<theta>2 v" by auto
472     with no_new_vars show ?thesis unfolding \<sigma>
473       by (auto simp:elim_def)
474   next
475     assume empty[simp]: "\<theta>2 =\<^sub>s []"
477     have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
478       by (rule compose_eqv) auto
479     also have "\<dots> =\<^sub>s \<theta>1" by auto
480     finally have "\<sigma> =\<^sub>s \<theta>1" .
482     from ih1 show ?thesis
483     proof
484       assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
485       with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
486       show ?thesis by auto
487     next
488       note `\<sigma> =\<^sub>s \<theta>1`
489       also assume "\<theta>1 =\<^sub>s []"
490       finally show ?thesis ..
491     qed
492   qed
493 qed
496 subsection {* Termination proof *}
498 termination unify
499 proof
500   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
501                            \<lambda>(M, N). size M]"
502   show "wf ?R" by simp
504   fix M N M' N'
505   show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
506     by (rule measures_lesseq) (auto intro: card_mono)
508   fix \<theta>                                   -- "Outer call"
509   assume inner: "unify_dom (M, M')"
510     "unify M M' = Some \<theta>"
512   from unify_eliminates[OF inner]
513   show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
514   proof
515     -- {* Either a variable is eliminated \ldots *}
516     assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
517     then obtain v
518 	  where "elim \<theta> v"
519 	  and "v\<in>vars_of M \<union> vars_of M'" by auto
520     with unify_vars[OF inner]
521     have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
522 	  \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
523 	  by auto
525     thus ?thesis
526       by (auto intro!: measures_less intro: psubset_card_mono)
527   next
528     -- {* Or the substitution is empty *}
529     assume "\<theta> =\<^sub>s []"
530     hence "N \<triangleleft> \<theta> = N"
531 	  and "N' \<triangleleft> \<theta> = N'" by auto
532     thus ?thesis
533        by (auto intro!: measures_less intro: psubset_card_mono)
534   qed
535 qed
537 end