equal
deleted
inserted
replaced
342 "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L" |
342 "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L" |
343 apply (simp add: relcl_def) |
343 apply (simp add: relcl_def) |
344 apply (blast intro: clD cl_in_lattice) |
344 apply (blast intro: clD cl_in_lattice) |
345 done |
345 done |
346 |
346 |
347 lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)" |
347 lemma refl_relcl: "lattice L ==> refl (relcl L)" |
348 by (simp add: reflI relcl_def subset_cl [THEN subsetD]) |
348 by (simp add: refl_onI relcl_def subset_cl [THEN subsetD]) |
349 |
349 |
350 lemma trans_relcl: "lattice L ==> trans (relcl L)" |
350 lemma trans_relcl: "lattice L ==> trans (relcl L)" |
351 by (blast intro: relcl_trans transI) |
351 by (blast intro: relcl_trans transI) |
352 |
352 |
353 lemma lattice_latticeof: "lattice (latticeof r)" |
353 lemma lattice_latticeof: "lattice (latticeof r)" |
360 apply (simp only: UN_in_lattice) |
360 apply (simp only: UN_in_lattice) |
361 done |
361 done |
362 |
362 |
363 text{*Equation (4.71) of Meier's thesis. He gives no proof.*} |
363 text{*Equation (4.71) of Meier's thesis. He gives no proof.*} |
364 lemma cl_latticeof: |
364 lemma cl_latticeof: |
365 "[|refl UNIV r; trans r|] |
365 "[|refl r; trans r|] |
366 ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" |
366 ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" |
367 apply (rule equalityI) |
367 apply (rule equalityI) |
368 apply (rule cl_least) |
368 apply (rule cl_least) |
369 apply (simp (no_asm_use) add: latticeof_def trans_def, blast) |
369 apply (simp (no_asm_use) add: latticeof_def trans_def, blast) |
370 apply (simp add: latticeof_def refl_def, blast) |
370 apply (simp add: latticeof_def refl_on_def, blast) |
371 apply (simp add: latticeof_def, clarify) |
371 apply (simp add: latticeof_def, clarify) |
372 apply (unfold cl_def, blast) |
372 apply (unfold cl_def, blast) |
373 done |
373 done |
374 |
374 |
375 text{*Related to (4.71).*} |
375 text{*Related to (4.71).*} |
398 cl_latticeof [OF refl_relcl trans_relcl]) |
398 cl_latticeof [OF refl_relcl trans_relcl]) |
399 apply (simp add: relcl_def) |
399 apply (simp add: relcl_def) |
400 done |
400 done |
401 |
401 |
402 theorem relcl_latticeof_eq: |
402 theorem relcl_latticeof_eq: |
403 "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r" |
403 "[|refl r; trans r|] ==> relcl (latticeof r) = r" |
404 by (simp add: relcl_def cl_latticeof) |
404 by (simp add: relcl_def cl_latticeof) |
405 |
405 |
406 |
406 |
407 subsubsection {*Decoupling Theorems*} |
407 subsubsection {*Decoupling Theorems*} |
408 |
408 |