Experimenting with interpretations of "definition".
authorballarin
Fri Dec 22 14:03:30 2006 +0100 (2006-12-22)
changeset 218969a7949815a84
parent 21895 6cbc0f69a21c
child 21897 d0c67d715deb
Experimenting with interpretations of "definition".
NEWS
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Ring.thy
     1.1 --- a/NEWS	Thu Dec 21 13:55:15 2006 +0100
     1.2 +++ b/NEWS	Fri Dec 22 14:03:30 2006 +0100
     1.3 @@ -710,8 +710,11 @@
     1.4  * Order and lattice theory no longer based on records.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Renamed lemmas least_carrier -> least_closed and
     1.8 +greatest_carrier -> greatest_closed.  INCOMPATIBILITY.
     1.9 +
    1.10  * Method algebra is now set up via an attribute.  For examples see
    1.11 -CRing.thy.  INCOMPATIBILITY: the method is now weaker on combinations
    1.12 +Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
    1.13  of algebraic structures.
    1.14  
    1.15  * Renamed `CRing.thy' to `Ring.thy'.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Dec 21 13:55:15 2006 +0100
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Dec 22 14:03:30 2006 +0100
     2.3 @@ -102,7 +102,48 @@
     2.4  apply clarsimp
     2.5  done
     2.6  
     2.7 -interpretation total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
     2.8 +lemma less_int:
     2.9 +  "order_syntax.less (op \<le>::[int, int] => bool) = (op <)"
    2.10 +  by (auto simp add: expand_fun_eq order_syntax.less_def)
    2.11 +
    2.12 +lemma join_int:
    2.13 +  "order_syntax.join (UNIV::int set) (op \<le>) = max"
    2.14 +  apply (simp add: expand_fun_eq max_def)
    2.15 +  apply (rule+)
    2.16 +  apply (rule lattice.joinI)
    2.17 +  apply (simp add: int_le_total_order total_order.axioms)
    2.18 +  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
    2.19 +  apply arith
    2.20 +  apply simp apply simp
    2.21 +  apply (rule lattice.joinI)
    2.22 +  apply (simp add: int_le_total_order total_order.axioms)
    2.23 +  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
    2.24 +  apply arith
    2.25 +  apply simp apply simp
    2.26 +  done
    2.27 +
    2.28 +lemma meet_int:
    2.29 +  "order_syntax.meet (UNIV::int set) (op \<le>) = min"
    2.30 +  apply (simp add: expand_fun_eq min_def)
    2.31 +  apply (rule+)
    2.32 +  apply (rule lattice.meetI)
    2.33 +  apply (simp add: int_le_total_order total_order.axioms)
    2.34 +  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
    2.35 +  apply arith
    2.36 +  apply simp apply simp
    2.37 +  apply (rule lattice.meetI)
    2.38 +  apply (simp add: int_le_total_order total_order.axioms)
    2.39 +  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
    2.40 +  apply arith
    2.41 +  apply simp apply simp
    2.42 +  done
    2.43 +
    2.44 +text {* Interpretation unfolding @{text less}, @{text join} and @{text
    2.45 +  meet} since they have natural representations in @{typ int}. *}
    2.46 +
    2.47 +interpretation 
    2.48 +  int [unfolded less_int join_int meet_int]:
    2.49 +  total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
    2.50  
    2.51  
    2.52  subsubsection {* Generated Ideals of @{text "\<Z>"} *}
     3.1 --- a/src/HOL/Algebra/Lattice.thy	Thu Dec 21 13:55:15 2006 +0100
     3.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Dec 22 14:03:30 2006 +0100
     3.3 @@ -34,7 +34,7 @@
     3.4  text {* Upper and lower bounds of a set. *}
     3.5  
     3.6  definition (in order_syntax)
     3.7 -  Upper where
     3.8 +  Upper :: "'a set => 'a set" where
     3.9    "Upper A == {u. (ALL x. x \<in> A \<inter> L --> x \<sqsubseteq> u)} \<inter> L"
    3.10  
    3.11  definition (in order_syntax)
     4.1 --- a/src/HOL/Algebra/Ring.thy	Thu Dec 21 13:55:15 2006 +0100
     4.2 +++ b/src/HOL/Algebra/Ring.thy	Fri Dec 22 14:03:30 2006 +0100
     4.3 @@ -454,7 +454,7 @@
     4.4    also from R have "... = \<zero>" by (simp add: l_neg l_null)
     4.5    finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
     4.6    with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
     4.7 -  with R show ?thesis by (simp add: a_assoc r_neg )
     4.8 +  with R show ?thesis by (simp add: a_assoc r_neg)
     4.9  qed
    4.10  
    4.11  lemma (in ring) r_minus: