convert instance proofs to Isar style
authorhuffman
Tue Jul 03 18:42:09 2007 +0200 (2007-07-03)
changeset 23550d4f1d6ef119c
parent 23549 88190085bb82
child 23551 84f0996a530b
convert instance proofs to Isar style
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Jul 03 18:00:57 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Jul 03 18:42:09 2007 +0200
     1.3 @@ -234,12 +234,16 @@
     1.4  instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
     1.5  
     1.6  instance ordered_semiring_strict \<subseteq> ordered_semiring
     1.7 -  apply (intro_classes)
     1.8 -  apply (cases "a < b & 0 < c")
     1.9 -  apply (auto simp add: mult_strict_left_mono order_less_le)
    1.10 -  apply (auto simp add: mult_strict_left_mono order_le_less)
    1.11 -  apply (simp add: mult_strict_right_mono)
    1.12 -  done
    1.13 +proof
    1.14 +  fix a b c :: 'a
    1.15 +  assume A: "a \<le> b" "0 \<le> c"
    1.16 +  from A show "c * a \<le> c * b"
    1.17 +    unfolding order_le_less
    1.18 +    using mult_strict_left_mono by auto
    1.19 +  from A show "a * c \<le> b * c"
    1.20 +    unfolding order_le_less
    1.21 +    using mult_strict_right_mono by auto
    1.22 +qed
    1.23  
    1.24  class mult_mono1 = times + zero + ord +
    1.25    assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
    1.26 @@ -258,26 +262,29 @@
    1.27  instance pordered_comm_semiring \<subseteq> pordered_semiring
    1.28  proof
    1.29    fix a b c :: 'a
    1.30 -  assume A: "a <= b" "0 <= c"
    1.31 -  with mult_mono show "c * a <= c * b" .
    1.32 -
    1.33 -  from mult_commute have "a * c = c * a" ..
    1.34 -  also from mult_mono A have "\<dots> <= c * b" .
    1.35 -  also from mult_commute have "c * b = b * c" ..
    1.36 -  finally show "a * c <= b * c" .
    1.37 +  assume "a \<le> b" "0 \<le> c"
    1.38 +  thus "c * a \<le> c * b" by (rule mult_mono)
    1.39 +  thus "a * c \<le> b * c" by (simp only: mult_commute)
    1.40  qed
    1.41  
    1.42  instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
    1.43  
    1.44  instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict
    1.45 -by (intro_classes, insert mult_strict_mono, simp_all add: mult_commute, blast+)
    1.46 +proof
    1.47 +  fix a b c :: 'a
    1.48 +  assume "a < b" "0 < c"
    1.49 +  thus "c * a < c * b" by (rule mult_strict_mono)
    1.50 +  thus "a * c < b * c" by (simp only: mult_commute)
    1.51 +qed
    1.52  
    1.53  instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring
    1.54 -apply (intro_classes)
    1.55 -apply (cases "a < b & 0 < c")
    1.56 -apply (auto simp add: mult_strict_left_mono order_less_le)
    1.57 -apply (auto simp add: mult_strict_left_mono order_le_less)
    1.58 -done
    1.59 +proof
    1.60 +  fix a b c :: 'a
    1.61 +  assume "a \<le> b" "0 \<le> c"
    1.62 +  thus "c * a \<le> c * b"
    1.63 +    unfolding order_le_less
    1.64 +    using mult_strict_mono by auto
    1.65 +qed
    1.66  
    1.67  class pordered_ring = ring + pordered_cancel_semiring 
    1.68  
    1.69 @@ -297,9 +304,12 @@
    1.70   *)
    1.71  class ordered_ring = ring + ordered_semiring + lordered_ab_group + abs_if
    1.72  
    1.73 -instance ordered_ring \<subseteq> lordered_ring 
    1.74 -  apply (intro_classes)
    1.75 -  by (simp add: abs_if sup_eq_if)
    1.76 +instance ordered_ring \<subseteq> lordered_ring
    1.77 +proof
    1.78 +  fix x :: 'a
    1.79 +  show "\<bar>x\<bar> = sup x (- x)"
    1.80 +    by (simp only: abs_if sup_eq_if)
    1.81 +qed
    1.82  
    1.83  class ordered_ring_strict = ring + ordered_semiring_strict + lordered_ab_group + abs_if
    1.84