326 lemmas [rule del] = min_max.le_infI min_max.le_supI |
326 lemmas [rule del] = min_max.le_infI min_max.le_supI |
327 min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2 |
327 min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2 |
328 min_max.le_infI1 min_max.le_infI2 |
328 min_max.le_infI1 min_max.le_infI2 |
329 |
329 |
330 |
330 |
331 subsection {* Complete lattices *} |
|
332 |
|
333 class complete_lattice = lattice + bot + top + |
|
334 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) |
|
335 and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
|
336 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" |
|
337 and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" |
|
338 assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" |
|
339 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" |
|
340 begin |
|
341 |
|
342 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}" |
|
343 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
|
344 |
|
345 lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}" |
|
346 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
|
347 |
|
348 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" |
|
349 unfolding Sup_Inf by auto |
|
350 |
|
351 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" |
|
352 unfolding Inf_Sup by auto |
|
353 |
|
354 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
|
355 by (auto intro: antisym Inf_greatest Inf_lower) |
|
356 |
|
357 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" |
|
358 by (auto intro: antisym Sup_least Sup_upper) |
|
359 |
|
360 lemma Inf_singleton [simp]: |
|
361 "\<Sqinter>{a} = a" |
|
362 by (auto intro: antisym Inf_lower Inf_greatest) |
|
363 |
|
364 lemma Sup_singleton [simp]: |
|
365 "\<Squnion>{a} = a" |
|
366 by (auto intro: antisym Sup_upper Sup_least) |
|
367 |
|
368 lemma Inf_insert_simp: |
|
369 "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" |
|
370 by (cases "A = {}") (simp_all, simp add: Inf_insert) |
|
371 |
|
372 lemma Sup_insert_simp: |
|
373 "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)" |
|
374 by (cases "A = {}") (simp_all, simp add: Sup_insert) |
|
375 |
|
376 lemma Inf_binary: |
|
377 "\<Sqinter>{a, b} = a \<sqinter> b" |
|
378 by (simp add: Inf_insert_simp) |
|
379 |
|
380 lemma Sup_binary: |
|
381 "\<Squnion>{a, b} = a \<squnion> b" |
|
382 by (simp add: Sup_insert_simp) |
|
383 |
|
384 lemma bot_def: |
|
385 "bot = \<Squnion>{}" |
|
386 by (auto intro: antisym Sup_least) |
|
387 |
|
388 lemma top_def: |
|
389 "top = \<Sqinter>{}" |
|
390 by (auto intro: antisym Inf_greatest) |
|
391 |
|
392 lemma sup_bot [simp]: |
|
393 "x \<squnion> bot = x" |
|
394 using bot_least [of x] by (simp add: le_iff_sup sup_commute) |
|
395 |
|
396 lemma inf_top [simp]: |
|
397 "x \<sqinter> top = x" |
|
398 using top_greatest [of x] by (simp add: le_iff_inf inf_commute) |
|
399 |
|
400 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
401 "SUPR A f == \<Squnion> (f ` A)" |
|
402 |
|
403 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
404 "INFI A f == \<Sqinter> (f ` A)" |
|
405 |
|
406 end |
|
407 |
|
408 syntax |
|
409 "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) |
|
410 "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10) |
|
411 "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10) |
|
412 "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10) |
|
413 |
|
414 translations |
|
415 "SUP x y. B" == "SUP x. SUP y. B" |
|
416 "SUP x. B" == "CONST SUPR UNIV (%x. B)" |
|
417 "SUP x. B" == "SUP x:UNIV. B" |
|
418 "SUP x:A. B" == "CONST SUPR A (%x. B)" |
|
419 "INF x y. B" == "INF x. INF y. B" |
|
420 "INF x. B" == "CONST INFI UNIV (%x. B)" |
|
421 "INF x. B" == "INF x:UNIV. B" |
|
422 "INF x:A. B" == "CONST INFI A (%x. B)" |
|
423 |
|
424 (* To avoid eta-contraction of body: *) |
|
425 print_translation {* |
|
426 let |
|
427 fun btr' syn (A :: Abs abs :: ts) = |
|
428 let val (x,t) = atomic_abs_tr' abs |
|
429 in list_comb (Syntax.const syn $ x $ A $ t, ts) end |
|
430 val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const |
|
431 in |
|
432 [(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")] |
|
433 end |
|
434 *} |
|
435 |
|
436 context complete_lattice |
|
437 begin |
|
438 |
|
439 lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)" |
|
440 by (auto simp add: SUPR_def intro: Sup_upper) |
|
441 |
|
442 lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u" |
|
443 by (auto simp add: SUPR_def intro: Sup_least) |
|
444 |
|
445 lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i" |
|
446 by (auto simp add: INFI_def intro: Inf_lower) |
|
447 |
|
448 lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)" |
|
449 by (auto simp add: INFI_def intro: Inf_greatest) |
|
450 |
|
451 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M" |
|
452 by (auto intro: antisym SUP_leI le_SUPI) |
|
453 |
|
454 lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M" |
|
455 by (auto intro: antisym INF_leI le_INFI) |
|
456 |
|
457 end |
|
458 |
|
459 |
|
460 subsection {* Bool as lattice *} |
331 subsection {* Bool as lattice *} |
461 |
332 |
462 instantiation bool :: distrib_lattice |
333 instantiation bool :: distrib_lattice |
463 begin |
334 begin |
464 |
335 |
520 end |
369 end |
521 |
370 |
522 instance "fun" :: (type, distrib_lattice) distrib_lattice |
371 instance "fun" :: (type, distrib_lattice) distrib_lattice |
523 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
372 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
524 |
373 |
525 instantiation "fun" :: (type, complete_lattice) complete_lattice |
|
526 begin |
|
527 |
|
528 definition |
|
529 Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})" |
|
530 |
|
531 definition |
|
532 Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})" |
|
533 |
|
534 instance |
|
535 by intro_classes |
|
536 (auto simp add: Inf_fun_def Sup_fun_def le_fun_def |
|
537 intro: Inf_lower Sup_upper Inf_greatest Sup_least) |
|
538 |
|
539 end |
|
540 |
|
541 lemma Inf_empty_fun: |
|
542 "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})" |
|
543 by rule (auto simp add: Inf_fun_def) |
|
544 |
|
545 lemma Sup_empty_fun: |
|
546 "\<Squnion>{} = (\<lambda>_. \<Squnion>{})" |
|
547 by rule (auto simp add: Sup_fun_def) |
|
548 |
|
549 |
|
550 subsection {* Set as lattice *} |
|
551 |
|
552 lemma inf_set_eq: "A \<sqinter> B = A \<inter> B" |
|
553 apply (rule subset_antisym) |
|
554 apply (rule Int_greatest) |
|
555 apply (rule inf_le1) |
|
556 apply (rule inf_le2) |
|
557 apply (rule inf_greatest) |
|
558 apply (rule Int_lower1) |
|
559 apply (rule Int_lower2) |
|
560 done |
|
561 |
|
562 lemma sup_set_eq: "A \<squnion> B = A \<union> B" |
|
563 apply (rule subset_antisym) |
|
564 apply (rule sup_least) |
|
565 apply (rule Un_upper1) |
|
566 apply (rule Un_upper2) |
|
567 apply (rule Un_least) |
|
568 apply (rule sup_ge1) |
|
569 apply (rule sup_ge2) |
|
570 done |
|
571 |
|
572 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B" |
|
573 apply (fold inf_set_eq sup_set_eq) |
|
574 apply (erule mono_inf) |
|
575 done |
|
576 |
|
577 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)" |
|
578 apply (fold inf_set_eq sup_set_eq) |
|
579 apply (erule mono_sup) |
|
580 done |
|
581 |
|
582 lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S" |
|
583 apply (rule subset_antisym) |
|
584 apply (rule Inter_greatest) |
|
585 apply (erule Inf_lower) |
|
586 apply (rule Inf_greatest) |
|
587 apply (erule Inter_lower) |
|
588 done |
|
589 |
|
590 lemma Sup_set_eq: "\<Squnion>S = \<Union>S" |
|
591 apply (rule subset_antisym) |
|
592 apply (rule Sup_least) |
|
593 apply (erule Union_upper) |
|
594 apply (rule Union_least) |
|
595 apply (erule Sup_upper) |
|
596 done |
|
597 |
|
598 lemma top_set_eq: "top = UNIV" |
|
599 by (iprover intro!: subset_antisym subset_UNIV top_greatest) |
|
600 |
|
601 lemma bot_set_eq: "bot = {}" |
|
602 by (iprover intro!: subset_antisym empty_subsetI bot_least) |
|
603 |
|
604 |
374 |
605 text {* redundant bindings *} |
375 text {* redundant bindings *} |
606 |
376 |
607 lemmas inf_aci = inf_ACI |
377 lemmas inf_aci = inf_ACI |
608 lemmas sup_aci = sup_ACI |
378 lemmas sup_aci = sup_ACI |
609 |
379 |
610 no_notation |
380 no_notation |
611 less_eq (infix "\<sqsubseteq>" 50) and |
381 less_eq (infix "\<sqsubseteq>" 50) and |
612 less (infix "\<sqsubset>" 50) and |
382 less (infix "\<sqsubset>" 50) and |
613 inf (infixl "\<sqinter>" 70) and |
383 inf (infixl "\<sqinter>" 70) and |
614 sup (infixl "\<squnion>" 65) and |
384 sup (infixl "\<squnion>" 65) |
615 Inf ("\<Sqinter>_" [900] 900) and |
385 |
616 Sup ("\<Squnion>_" [900] 900) |
386 end |
617 |
|
618 end |
|