src/HOL/Library/Finite_Lattice.thy
changeset 51489 f738e6dbd844
parent 51115 7dbd6832a689
child 52729 412c9e0381a1
     1.1 --- a/src/HOL/Library/Finite_Lattice.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -39,6 +39,30 @@
     1.4  by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
     1.5  -- "Derived definition of @{const top}."
     1.6  
     1.7 +lemma finite_lattice_complete_Inf_empty:
     1.8 +  "Inf {} = (top :: 'a::finite_lattice_complete)"
     1.9 +  by (simp add: Inf_def)
    1.10 +
    1.11 +lemma finite_lattice_complete_Sup_empty:
    1.12 +  "Sup {} = (bot :: 'a::finite_lattice_complete)"
    1.13 +  by (simp add: Sup_def)
    1.14 +
    1.15 +lemma finite_lattice_complete_Inf_insert:
    1.16 +  fixes A :: "'a::finite_lattice_complete set"
    1.17 +  shows "Inf (insert x A) = inf x (Inf A)"
    1.18 +proof -
    1.19 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> _" by (fact comp_fun_idem_inf)
    1.20 +  show ?thesis by (simp add: Inf_def)
    1.21 +qed
    1.22 +
    1.23 +lemma finite_lattice_complete_Sup_insert:
    1.24 +  fixes A :: "'a::finite_lattice_complete set"
    1.25 +  shows "Sup (insert x A) = sup x (Sup A)"
    1.26 +proof -
    1.27 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> _" by (fact comp_fun_idem_sup)
    1.28 +  show ?thesis by (simp add: Sup_def)
    1.29 +qed
    1.30 +
    1.31  text {* The definitional assumptions
    1.32  on the operators @{const Inf} and @{const Sup}
    1.33  of class @{class finite_lattice_complete}
    1.34 @@ -47,19 +71,19 @@
    1.35  
    1.36  lemma finite_lattice_complete_Inf_lower:
    1.37    "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
    1.38 -unfolding Inf_def by (metis finite_code le_inf_iff fold_inf_le_inf)
    1.39 +  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
    1.40  
    1.41  lemma finite_lattice_complete_Inf_greatest:
    1.42    "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
    1.43 -unfolding Inf_def by (metis finite_code inf_le_fold_inf inf_top_right)
    1.44 +  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)
    1.45  
    1.46  lemma finite_lattice_complete_Sup_upper:
    1.47    "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
    1.48 -unfolding Sup_def by (metis finite_code le_sup_iff sup_le_fold_sup)
    1.49 +  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)
    1.50  
    1.51  lemma finite_lattice_complete_Sup_least:
    1.52    "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
    1.53 -unfolding Sup_def by (metis finite_code fold_sup_le_sup sup_bot_right)
    1.54 +  using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)
    1.55  
    1.56  instance finite_lattice_complete \<subseteq> complete_lattice
    1.57  proof