src/HOL/Finite_Set.thy
changeset 23949 06a988643235
parent 23878 bd651ecd4b8a
child 24163 9e6a2a7da86a
equal deleted 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*}