src/HOL/Finite_Set.thy
 changeset 23949 06a988643235 parent 23878 bd651ecd4b8a child 24163 9e6a2a7da86a
equal inserted replaced
23948:261bd4678076 23949:06a988643235
`  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*}`