2682 definition |
2682 definition |
2683 Max :: "'a set \<Rightarrow> 'a\<Colon>linorder" |
2683 Max :: "'a set \<Rightarrow> 'a\<Colon>linorder" |
2684 where |
2684 where |
2685 "Max = fold1 max" |
2685 "Max = fold1 max" |
2686 |
2686 |
2687 lemma Linorder_Min: |
2687 interpretation |
2688 "Linorder.Min (op \<le>) = Min" |
2688 Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"] |
2689 proof |
2689 where |
2690 fix A :: "'a set" |
2690 "Linorder.Min (op \<le>) = Min" and "Linorder.Max (op \<le>) = Max" |
2691 show "Linorder.Min (op \<le>) A = Min A" |
2691 proof - |
2692 by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_axioms] |
2692 show "Linorder (op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool) op <" |
2693 ord_class.min) |
2693 by (rule Linorder.intro, rule linorder_axioms) |
2694 qed |
2694 have "Linorder (op \<le> \<Colon> 'b \<Rightarrow> 'b \<Rightarrow> bool) op <" |
2695 |
2695 by (rule Linorder.intro, rule linorder_axioms) |
2696 lemma Linorder_Max: |
2696 then interpret Linorder1: Linorder ["op \<le> \<Colon> 'b \<Rightarrow> 'b \<Rightarrow> bool" "op <"] . |
2697 "Linorder.Max (op \<le>) = Max" |
2697 show "Linorder1.Min = Min" by (simp add: Min_def Linorder1.Min_def ord_class.min) |
2698 proof |
2698 have "Linorder (op \<le> \<Colon> 'c \<Rightarrow> 'c \<Rightarrow> bool) op <" |
2699 fix A :: "'a set" |
2699 by (rule Linorder.intro, rule linorder_axioms) |
2700 show "Linorder.Max (op \<le>) A = Max A" |
2700 then interpret Linorder2: Linorder ["op \<le> \<Colon> 'c \<Rightarrow> 'c \<Rightarrow> bool" "op <"] . |
2701 by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms] |
2701 show "Linorder2.Max = Max" by (simp add: Max_def Linorder2.Max_def ord_class.max) |
2702 ord_class.max) |
2702 qed |
2703 qed |
2703 |
2704 |
2704 interpretation |
2705 (*FIXME: temporary solution - doesn't work properly*) |
|
2706 interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]: |
|
2707 Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"] |
2705 Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"] |
|
2706 proof - |
|
2707 show "Linorder_ab_semigroup_add (op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool) (op <) (op +)" |
2708 by (rule Linorder_ab_semigroup_add.intro, |
2708 by (rule Linorder_ab_semigroup_add.intro, |
2709 rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms) |
2709 rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms) |
2710 hide const Min Max |
2710 qed |
2711 |
|
2712 interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]: |
|
2713 Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"] |
|
2714 by (rule Linorder.intro, rule linorder_axioms) |
|
2715 declare Min_singleton [simp] |
|
2716 declare Max_singleton [simp] |
|
2717 declare Min_insert [simp] |
|
2718 declare Max_insert [simp] |
|
2719 declare Min_in [simp] |
|
2720 declare Max_in [simp] |
|
2721 declare Min_le [simp] |
|
2722 declare Max_ge [simp] |
|
2723 declare Min_ge_iff [simp] |
|
2724 declare Max_le_iff [simp] |
|
2725 declare Min_gr_iff [simp] |
|
2726 declare Max_less_iff [simp] |
|
2727 declare Max_less_iff [simp] |
|
2728 |
2711 |
2729 |
2712 |
2730 subsection {* Class @{text finite} *} |
2713 subsection {* Class @{text finite} *} |
2731 |
2714 |
2732 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} |
2715 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} |