some stuff is now redundant.
authornipkow
Thu Feb 10 19:14:35 2005 +0100 (2005-02-10)
changeset 15526748ebc63b807
parent 15525 396268ad58b3
child 15527 95db9cf4b047
some stuff is now redundant.
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Feb 10 18:51:54 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 10 19:14:35 2005 +0100
     1.3 @@ -2200,37 +2200,11 @@
     1.4  apply(auto simp:max_def)
     1.5  done
     1.6  
     1.7 -lemma partial_order_order:
     1.8 - "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
     1.9 -apply(rule partial_order.intro)
    1.10 -apply(simp_all)
    1.11 -done
    1.12 -
    1.13 -lemma lower_semilattice_lin_min:
    1.14 -  "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.15 -apply(rule lower_semilattice.intro)
    1.16 -apply(rule partial_order_order)
    1.17 -apply(rule lower_semilattice_axioms.intro)
    1.18 -apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.19 -apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.20 -apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.21 -done
    1.22 -
    1.23 -lemma upper_semilattice_lin_min:
    1.24 -  "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.25 -apply(rule upper_semilattice.intro)
    1.26 -apply(rule partial_order_order)
    1.27 -apply(rule upper_semilattice_axioms.intro)
    1.28 -apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.29 -apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.30 -apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.31 -done
    1.32 -
    1.33  lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
    1.34  apply(rule Lattice.intro)
    1.35  apply(rule partial_order_order)
    1.36  apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    1.37 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min])
    1.38 +apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    1.39  done
    1.40  
    1.41  lemma Distrib_Lattice_min_max:
    1.42 @@ -2238,23 +2212,8 @@
    1.43  apply(rule Distrib_Lattice.intro)
    1.44  apply(rule partial_order_order)
    1.45  apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    1.46 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min])
    1.47 -apply(rule distrib_lattice_axioms.intro)
    1.48 -apply(rule_tac x=x and y=y in linorder_le_cases)
    1.49 -apply(rule_tac x=x and y=z in linorder_le_cases)
    1.50 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.51 -apply(simp add:min_def max_def)
    1.52 -apply(simp add:min_def max_def)
    1.53 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.54 -apply(simp add:min_def max_def)
    1.55 -apply(simp add:min_def max_def)
    1.56 -apply(rule_tac x=x and y=z in linorder_le_cases)
    1.57 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.58 -apply(simp add:min_def max_def)
    1.59 -apply(simp add:min_def max_def)
    1.60 -apply(rule_tac x=y and y=z in linorder_le_cases)
    1.61 -apply(simp add:min_def max_def)
    1.62 -apply(simp add:min_def max_def)
    1.63 +apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    1.64 +apply(rule distrib_lattice.axioms[OF distrib_lattice_min_max])
    1.65  done
    1.66  
    1.67  text{* Now we instantiate the recursion equations and declare them