Used locale interpretations everywhere.
authornipkow
Wed Apr 20 17:19:18 2005 +0200 (2005-04-20)
changeset 157806744bba5561d
parent 15779 aed221aff642
child 15781 70d559802ae3
Used locale interpretations everywhere.
src/HOL/Finite_Set.thy
src/HOL/Orderings.ML
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Apr 20 16:03:17 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Apr 20 17:19:18 2005 +0200
     1.3 @@ -516,23 +516,10 @@
     1.4  
     1.5  interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
     1.6    apply -
     1.7 -   apply (fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
     1.8 -  apply (fastsimp intro: ACe_axioms.intro mult_assoc ab_semigroup_mult.mult_commute)
     1.9 +   apply (fast intro: ACf.intro mult_assoc mult_commute)
    1.10 +  apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute)
    1.11    done
    1.12  
    1.13 -(*
    1.14 -lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.15 -by(fastsimp intro: ACf.intro add_assoc add_commute)
    1.16 -
    1.17 -lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
    1.18 -by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
    1.19 -
    1.20 -lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.21 -by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
    1.22 -
    1.23 -lemma ACe_mult: "ACe (op * ) (1::'a::comm_monoid_mult)"
    1.24 -by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
    1.25 -*)
    1.26  
    1.27  subsubsection{*From @{term foldSet} to @{term fold}*}
    1.28  
    1.29 @@ -2149,7 +2136,7 @@
    1.30  
    1.31  subsubsection{* Fold laws in lattices *}
    1.32  
    1.33 -lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
    1.34 +lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
    1.35  apply(unfold Sup_def Inf_def)
    1.36  apply(subgoal_tac "EX a. a:A")
    1.37  prefer 2 apply blast
    1.38 @@ -2159,13 +2146,13 @@
    1.39  apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.40  done
    1.41  
    1.42 -lemma (in Lattice) sup_Inf_absorb:
    1.43 +lemma (in Lattice) sup_Inf_absorb[simp]:
    1.44    "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
    1.45  apply(subst sup_commute)
    1.46  apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
    1.47  done
    1.48  
    1.49 -lemma (in Lattice) inf_Sup_absorb:
    1.50 +lemma (in Lattice) inf_Sup_absorb[simp]:
    1.51    "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
    1.52  by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.53  
    1.54 @@ -2260,51 +2247,41 @@
    1.55  apply(auto simp:max_def)
    1.56  done
    1.57  
    1.58 -interpretation AC_min [rule del]: ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    1.59 +interpretation AC_min [rule del]:
    1.60 +  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    1.61  apply(rule ACIfSL_axioms.intro)
    1.62  apply(auto simp:min_def)
    1.63  done
    1.64  
    1.65 -interpretation AC_min [rule del]: ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    1.66 +interpretation AC_min [rule del]:
    1.67 +  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
    1.68  apply(rule ACIfSLlin_axioms.intro)
    1.69  apply(auto simp:min_def)
    1.70  done
    1.71  
    1.72 -interpretation AC_max [rule del]: ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
    1.73 +interpretation AC_max [rule del]:
    1.74 +  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
    1.75  apply(rule ACIfSL_axioms.intro)
    1.76  apply(auto simp:max_def)
    1.77  done
    1.78  
    1.79 -interpretation AC_max [rule del]: ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
    1.80 +interpretation AC_max [rule del]:
    1.81 +  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
    1.82  apply(rule ACIfSLlin_axioms.intro)
    1.83  apply(auto simp:max_def)
    1.84  done
    1.85  
    1.86 -lemma Lattice_min_max [rule del]: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
    1.87 -apply(rule Lattice.intro)
    1.88 -apply(rule partial_order_order)
    1.89 -apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    1.90 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    1.91 +interpretation min_max [rule del]:
    1.92 +  Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
    1.93 +apply -
    1.94 +apply(rule Min_def)
    1.95 +apply(rule Max_def)
    1.96  done
    1.97  
    1.98 -lemma Distrib_Lattice_min_max [rule del]:
    1.99 - "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
   1.100 -apply(rule Distrib_Lattice.intro)
   1.101 -apply(rule partial_order_order)
   1.102 -apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
   1.103 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
   1.104 -apply(rule distrib_lattice.axioms[OF distrib_lattice_min_max])
   1.105 -done
   1.106  
   1.107 -interpretation Lattice_min_max [rule del]:
   1.108 -  Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   1.109 -using Lattice_min_max
   1.110 -by (auto dest: Lattice.axioms)
   1.111 -
   1.112 -interpretation Lattice_min_max [rule del]:
   1.113 -  Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   1.114 -using Distrib_Lattice_min_max
   1.115 -by (fast dest: Distrib_Lattice.axioms)
   1.116 +interpretation min_max [rule del]:
   1.117 +  Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
   1.118 +.
   1.119  
   1.120  text {* Classical rules from the locales are deleted in the above
   1.121    interpretations, since they interfere with the claset setup for
   1.122 @@ -2356,13 +2333,4 @@
   1.123    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
   1.124  by(simp add: Max_def AC_max.fold1_below_iff)
   1.125  
   1.126 -lemma Min_le_Max:
   1.127 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
   1.128 -by(simp add: Min_def Max_def Lattice_min_max.Inf_le_Sup)
   1.129 -
   1.130 -lemma max_Min2_distrib:
   1.131 -  "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
   1.132 -  max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
   1.133 -by(simp add: Min_def Lattice_min_max.sup_Inf2_distrib)
   1.134 -
   1.135  end
     2.1 --- a/src/HOL/Orderings.ML	Wed Apr 20 16:03:17 2005 +0200
     2.2 +++ b/src/HOL/Orderings.ML	Wed Apr 20 17:19:18 2005 +0200
     2.3 @@ -39,9 +39,7 @@
     2.4  val le_maxI1 = thm "le_maxI1";
     2.5  val le_maxI2 = thm "le_maxI2";
     2.6  val less_max_iff_disj = thm "less_max_iff_disj";
     2.7 -val max_le_iff_conj = thm "max_le_iff_conj";
     2.8  val max_less_iff_conj = thm "max_less_iff_conj";
     2.9 -val le_min_iff_conj = thm "le_min_iff_conj";
    2.10  val min_less_iff_conj = thm "min_less_iff_conj";
    2.11  val min_le_iff_disj = thm "min_le_iff_disj";
    2.12  val min_less_iff_disj = thm "min_less_iff_disj";
     3.1 --- a/src/HOL/Orderings.thy	Wed Apr 20 16:03:17 2005 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Wed Apr 20 17:19:18 2005 +0200
     3.3 @@ -93,8 +93,8 @@
     3.4  
     3.5  text{* Connection to locale: *}
     3.6  
     3.7 -lemma partial_order_order:
     3.8 - "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
     3.9 +interpretation order[rule del]:
    3.10 +  partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"]
    3.11  apply(rule partial_order.intro)
    3.12  apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
    3.13  done
    3.14 @@ -226,6 +226,16 @@
    3.15  axclass linorder < order
    3.16    linorder_linear: "x <= y | y <= x"
    3.17  
    3.18 +(* Could (should?) follow automatically from the interpretation of
    3.19 +   partial_order by class order. rule del is needed because two copies
    3.20 +   of refl with classes order and linorder confuse blast (and are pointless)*)
    3.21 +interpretation order[rule del]:
    3.22 +  partial_order["op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool"]
    3.23 +apply(rule partial_order.intro)
    3.24 +apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
    3.25 +done
    3.26 +
    3.27 +
    3.28  lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
    3.29    apply (simp add: order_less_le)
    3.30    apply (insert linorder_linear, blast)
    3.31 @@ -388,39 +398,30 @@
    3.32  
    3.33  text{* Instantiate locales: *}
    3.34  
    3.35 -lemma lower_semilattice_lin_min:
    3.36 -  "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    3.37 -apply(rule lower_semilattice.intro)
    3.38 -apply(rule partial_order_order)
    3.39 +interpretation min_max [rule del]:
    3.40 +  lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    3.41 +apply -
    3.42  apply(rule lower_semilattice_axioms.intro)
    3.43  apply(simp add:min_def linorder_not_le order_less_imp_le)
    3.44  apply(simp add:min_def linorder_not_le order_less_imp_le)
    3.45  apply(simp add:min_def linorder_not_le order_less_imp_le)
    3.46  done
    3.47  
    3.48 -lemma upper_semilattice_lin_max:
    3.49 -  "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    3.50 -apply(rule upper_semilattice.intro)
    3.51 -apply(rule partial_order_order)
    3.52 +interpretation min_max [rule del]:
    3.53 +  upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    3.54 +apply -
    3.55  apply(rule upper_semilattice_axioms.intro)
    3.56  apply(simp add: max_def linorder_not_le order_less_imp_le)
    3.57  apply(simp add: max_def linorder_not_le order_less_imp_le)
    3.58  apply(simp add: max_def linorder_not_le order_less_imp_le)
    3.59  done
    3.60  
    3.61 -lemma lattice_min_max: "lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
    3.62 -apply(rule lattice.intro)
    3.63 -apply(rule partial_order_order)
    3.64 -apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    3.65 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    3.66 -done
    3.67 +interpretation min_max [rule del]:
    3.68 +  lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    3.69 +.
    3.70  
    3.71 -lemma distrib_lattice_min_max:
    3.72 - "distrib_lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
    3.73 -apply(rule distrib_lattice.intro)
    3.74 -apply(rule partial_order_order)
    3.75 -apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    3.76 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    3.77 +interpretation min_max [rule del]:
    3.78 +  distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    3.79  apply(rule distrib_lattice_axioms.intro)
    3.80  apply(rule_tac x=x and y=y in linorder_le_cases)
    3.81  apply(rule_tac x=x and y=z in linorder_le_cases)
    3.82 @@ -445,12 +446,8 @@
    3.83    apply (blast intro: order_trans)
    3.84    done
    3.85  
    3.86 -lemma le_maxI1: "(x::'a::linorder) <= max x y"
    3.87 -by(rule upper_semilattice.sup_ge1[OF upper_semilattice_lin_max])
    3.88 -
    3.89 -lemma le_maxI2: "(y::'a::linorder) <= max x y"
    3.90 -    -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *}
    3.91 -by(rule upper_semilattice.sup_ge2[OF upper_semilattice_lin_max])
    3.92 +lemmas le_maxI1 = min_max.sup_ge1
    3.93 +lemmas le_maxI2 = min_max.sup_ge2
    3.94  
    3.95  lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
    3.96    apply (simp add: max_def order_le_less)
    3.97 @@ -458,22 +455,18 @@
    3.98    apply (blast intro: order_less_trans)
    3.99    done
   3.100  
   3.101 -lemma max_le_iff_conj [simp]:
   3.102 -    "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"
   3.103 -by (rule upper_semilattice.above_sup_conv[OF upper_semilattice_lin_max])
   3.104 -
   3.105  lemma max_less_iff_conj [simp]:
   3.106      "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   3.107    apply (simp add: order_le_less max_def)
   3.108    apply (insert linorder_less_linear)
   3.109    apply (blast intro: order_less_trans)
   3.110    done
   3.111 -
   3.112 +(*
   3.113  lemma le_min_iff_conj [simp]:
   3.114      "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
   3.115      -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
   3.116  by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
   3.117 -
   3.118 +*)
   3.119  lemma min_less_iff_conj [simp]:
   3.120      "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   3.121    apply (simp add: order_le_less min_def)
   3.122 @@ -492,24 +485,24 @@
   3.123    apply (insert linorder_less_linear)
   3.124    apply (blast intro: order_less_trans)
   3.125    done
   3.126 -
   3.127 +(*
   3.128  lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
   3.129  by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
   3.130  
   3.131  lemma max_commute: "!!x::'a::linorder. max x y = max y x"
   3.132  by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
   3.133 -
   3.134 -lemmas max_ac = max_assoc max_commute
   3.135 -                mk_left_commute[of max,OF max_assoc max_commute]
   3.136 -
   3.137 +*)
   3.138 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   3.139 +               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   3.140 +(*
   3.141  lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
   3.142  by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
   3.143  
   3.144  lemma min_commute: "!!x::'a::linorder. min x y = min y x"
   3.145  by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
   3.146 -
   3.147 -lemmas min_ac = min_assoc min_commute
   3.148 -                mk_left_commute[of min,OF min_assoc min_commute]
   3.149 +*)
   3.150 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   3.151 +               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   3.152  
   3.153  lemma split_min:
   3.154      "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"