8 theory Lattices |
8 theory Lattices |
9 imports Orderings |
9 imports Orderings |
10 begin |
10 begin |
11 |
11 |
12 subsection{* Lattices *} |
12 subsection{* Lattices *} |
|
13 |
|
14 notation |
|
15 less_eq (infix "\<sqsubseteq>" 50) |
|
16 and |
|
17 less (infix "\<sqsubset>" 50) |
13 |
18 |
14 class lower_semilattice = order + |
19 class lower_semilattice = order + |
15 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
20 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
16 assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
21 assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
17 and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
22 and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
59 by blast |
64 by blast |
60 |
65 |
61 lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
66 lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
62 by (blast intro: antisym dest: eq_iff [THEN iffD1]) |
67 by (blast intro: antisym dest: eq_iff [THEN iffD1]) |
63 |
68 |
64 end |
69 lemma mono_inf: |
65 |
70 fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice" |
66 lemma mono_inf: "mono f \<Longrightarrow> f (inf A B) \<le> inf (f A) (f B)" |
71 shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" |
67 by (auto simp add: mono_def) |
72 by (auto simp add: mono_def intro: Lattices.inf_greatest) |
68 |
73 |
|
74 end |
69 |
75 |
70 context upper_semilattice |
76 context upper_semilattice |
71 begin |
77 begin |
72 |
78 |
73 lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
79 lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
91 by blast |
97 by blast |
92 |
98 |
93 lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
99 lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
94 by (blast intro: antisym dest: eq_iff [THEN iffD1]) |
100 by (blast intro: antisym dest: eq_iff [THEN iffD1]) |
95 |
101 |
96 end |
102 lemma mono_sup: |
97 |
103 fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice" |
98 lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) \<le> f (sup A B)" |
104 shows "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" |
99 by (auto simp add: mono_def) |
105 by (auto simp add: mono_def intro: Lattices.sup_least) |
|
106 |
|
107 end |
100 |
108 |
101 |
109 |
102 subsubsection{* Equational laws *} |
110 subsubsection{* Equational laws *} |
103 |
|
104 |
111 |
105 context lower_semilattice |
112 context lower_semilattice |
106 begin |
113 begin |
107 |
114 |
108 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
115 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
391 by (simp add: Sup_insert_simp) |
398 by (simp add: Sup_insert_simp) |
392 |
399 |
393 definition |
400 definition |
394 top :: 'a |
401 top :: 'a |
395 where |
402 where |
396 "top = Inf {}" |
403 "top = \<Sqinter>{}" |
397 |
404 |
398 definition |
405 definition |
399 bot :: 'a |
406 bot :: 'a |
400 where |
407 where |
401 "bot = Sup {}" |
408 "bot = \<Squnion>{}" |
402 |
409 |
403 lemma top_greatest [simp]: "x \<le> top" |
410 lemma top_greatest [simp]: "x \<le> top" |
404 by (unfold top_def, rule Inf_greatest, simp) |
411 by (unfold top_def, rule Inf_greatest, simp) |
405 |
412 |
406 lemma bot_least [simp]: "bot \<le> x" |
413 lemma bot_least [simp]: "bot \<le> x" |
407 by (unfold bot_def, rule Sup_least, simp) |
414 by (unfold bot_def, rule Sup_least, simp) |
408 |
415 |
409 definition |
416 definition |
410 SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
417 SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
411 where |
418 where |
412 "SUPR A f == Sup (f ` A)" |
419 "SUPR A f == \<Squnion> (f ` A)" |
413 |
420 |
414 definition |
421 definition |
415 INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
422 INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" |
416 where |
423 where |
417 "INFI A f == Inf (f ` A)" |
424 "INFI A f == \<Sqinter> (f ` A)" |
418 |
425 |
419 end |
426 end |
420 |
427 |
421 syntax |
428 syntax |
422 "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) |
429 "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10) |
471 |
478 |
472 |
479 |
473 subsection {* Bool as lattice *} |
480 subsection {* Bool as lattice *} |
474 |
481 |
475 instance bool :: distrib_lattice |
482 instance bool :: distrib_lattice |
476 inf_bool_eq: "inf P Q \<equiv> P \<and> Q" |
483 inf_bool_eq: "P \<sqinter> Q \<equiv> P \<and> Q" |
477 sup_bool_eq: "sup P Q \<equiv> P \<or> Q" |
484 sup_bool_eq: "P \<squnion> Q \<equiv> P \<or> Q" |
478 by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) |
485 by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) |
479 |
486 |
480 instance bool :: complete_lattice |
487 instance bool :: complete_lattice |
481 Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x" |
488 Inf_bool_def: "\<Sqinter>A \<equiv> \<forall>x\<in>A. x" |
482 Sup_bool_def: "Sup A \<equiv> \<exists>x\<in>A. x" |
489 Sup_bool_def: "\<Squnion>A \<equiv> \<exists>x\<in>A. x" |
483 by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def) |
490 by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def) |
484 |
491 |
485 lemma Inf_empty_bool [simp]: |
492 lemma Inf_empty_bool [simp]: |
486 "Inf {}" |
493 "\<Sqinter>{}" |
487 unfolding Inf_bool_def by auto |
494 unfolding Inf_bool_def by auto |
488 |
495 |
489 lemma not_Sup_empty_bool [simp]: |
496 lemma not_Sup_empty_bool [simp]: |
490 "\<not> Sup {}" |
497 "\<not> Sup {}" |
491 unfolding Sup_bool_def by auto |
498 unfolding Sup_bool_def by auto |
498 |
505 |
499 |
506 |
500 subsection {* Set as lattice *} |
507 subsection {* Set as lattice *} |
501 |
508 |
502 instance set :: (type) distrib_lattice |
509 instance set :: (type) distrib_lattice |
503 inf_set_eq: "inf A B \<equiv> A \<inter> B" |
510 inf_set_eq: "A \<sqinter> B \<equiv> A \<inter> B" |
504 sup_set_eq: "sup A B \<equiv> A \<union> B" |
511 sup_set_eq: "A \<squnion> B \<equiv> A \<union> B" |
505 by intro_classes (auto simp add: inf_set_eq sup_set_eq) |
512 by intro_classes (auto simp add: inf_set_eq sup_set_eq) |
506 |
513 |
507 lemmas [code func del] = inf_set_eq sup_set_eq |
514 lemmas [code func del] = inf_set_eq sup_set_eq |
508 |
515 |
509 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B" |
516 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B" |
515 apply (fold inf_set_eq sup_set_eq) |
522 apply (fold inf_set_eq sup_set_eq) |
516 apply (erule mono_sup) |
523 apply (erule mono_sup) |
517 done |
524 done |
518 |
525 |
519 instance set :: (type) complete_lattice |
526 instance set :: (type) complete_lattice |
520 Inf_set_def: "Inf S \<equiv> \<Inter>S" |
527 Inf_set_def: "\<Sqinter>S \<equiv> \<Inter>S" |
521 Sup_set_def: "Sup S \<equiv> \<Union>S" |
528 Sup_set_def: "\<Squnion>S \<equiv> \<Union>S" |
522 by intro_classes (auto simp add: Inf_set_def Sup_set_def) |
529 by intro_classes (auto simp add: Inf_set_def Sup_set_def) |
523 |
530 |
524 lemmas [code func del] = Inf_set_def Sup_set_def |
531 lemmas [code func del] = Inf_set_def Sup_set_def |
525 |
532 |
526 lemma top_set_eq: "top = UNIV" |
533 lemma top_set_eq: "top = UNIV" |
531 |
538 |
532 |
539 |
533 subsection {* Fun as lattice *} |
540 subsection {* Fun as lattice *} |
534 |
541 |
535 instance "fun" :: (type, lattice) lattice |
542 instance "fun" :: (type, lattice) lattice |
536 inf_fun_eq: "inf f g \<equiv> (\<lambda>x. inf (f x) (g x))" |
543 inf_fun_eq: "f \<sqinter> g \<equiv> (\<lambda>x. f x \<sqinter> g x)" |
537 sup_fun_eq: "sup f g \<equiv> (\<lambda>x. sup (f x) (g x))" |
544 sup_fun_eq: "f \<squnion> g \<equiv> (\<lambda>x. f x \<squnion> g x)" |
538 apply intro_classes |
545 apply intro_classes |
539 unfolding inf_fun_eq sup_fun_eq |
546 unfolding inf_fun_eq sup_fun_eq |
540 apply (auto intro: le_funI) |
547 apply (auto intro: le_funI) |
541 apply (rule le_funI) |
548 apply (rule le_funI) |
542 apply (auto dest: le_funD) |
549 apply (auto dest: le_funD) |
548 |
555 |
549 instance "fun" :: (type, distrib_lattice) distrib_lattice |
556 instance "fun" :: (type, distrib_lattice) distrib_lattice |
550 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
557 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
551 |
558 |
552 instance "fun" :: (type, complete_lattice) complete_lattice |
559 instance "fun" :: (type, complete_lattice) complete_lattice |
553 Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})" |
560 Inf_fun_def: "\<Sqinter>A \<equiv> (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})" |
554 Sup_fun_def: "Sup A \<equiv> (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})" |
561 Sup_fun_def: "\<Squnion>A \<equiv> (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})" |
555 by intro_classes |
562 by intro_classes |
556 (auto simp add: Inf_fun_def Sup_fun_def le_fun_def |
563 (auto simp add: Inf_fun_def Sup_fun_def le_fun_def |
557 intro: Inf_lower Sup_upper Inf_greatest Sup_least) |
564 intro: Inf_lower Sup_upper Inf_greatest Sup_least) |
558 |
565 |
559 lemmas [code func del] = Inf_fun_def Sup_fun_def |
566 lemmas [code func del] = Inf_fun_def Sup_fun_def |
560 |
567 |
561 lemma Inf_empty_fun: |
568 lemma Inf_empty_fun: |
562 "Inf {} = (\<lambda>_. Inf {})" |
569 "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})" |
563 by rule (auto simp add: Inf_fun_def) |
570 by rule (auto simp add: Inf_fun_def) |
564 |
571 |
565 lemma Sup_empty_fun: |
572 lemma Sup_empty_fun: |
566 "Sup {} = (\<lambda>_. Sup {})" |
573 "\<Squnion>{} = (\<lambda>_. \<Squnion>{})" |
567 by rule (auto simp add: Sup_fun_def) |
574 by rule (auto simp add: Sup_fun_def) |
568 |
575 |
569 lemma top_fun_eq: "top = (\<lambda>x. top)" |
576 lemma top_fun_eq: "top = (\<lambda>x. top)" |
570 by (iprover intro!: order_antisym le_funI top_greatest) |
577 by (iprover intro!: order_antisym le_funI top_greatest) |
571 |
578 |
577 |
584 |
578 lemmas inf_aci = inf_ACI |
585 lemmas inf_aci = inf_ACI |
579 lemmas sup_aci = sup_ACI |
586 lemmas sup_aci = sup_ACI |
580 |
587 |
581 no_notation |
588 no_notation |
582 inf (infixl "\<sqinter>" 70) |
589 less_eq (infix "\<sqsubseteq>" 50) |
583 |
590 and |
584 no_notation |
591 less (infix "\<sqsubset>" 50) |
585 sup (infixl "\<squnion>" 65) |
592 and |
586 |
593 inf (infixl "\<sqinter>" 70) |
587 no_notation |
594 and |
588 Inf ("\<Sqinter>_" [900] 900) |
595 sup (infixl "\<squnion>" 65) |
589 |
596 and |
590 no_notation |
597 Inf ("\<Sqinter>_" [900] 900) |
591 Sup ("\<Squnion>_" [900] 900) |
598 and |
592 |
599 Sup ("\<Squnion>_" [900] 900) |
593 end |
600 |
|
601 end |