doc-src/TutorialI/Types/Numbers.thy

 @{subgoals[display,indent=0,margin=65]}
 *};
 oops
 
 text{*
-@{thm[display] mult_le_mono[no_vars]}
-\rulename{mult_le_mono}
-
-@{thm[display] mult_less_mono1[no_vars]}
-\rulename{mult_less_mono1}
 
 @{thm[display] div_le_mono[no_vars]}
 \rulename{div_le_mono}
-
-@{thm[display] add_mult_distrib[no_vars]}
-\rulename{add_mult_distrib}
 
 @{thm[display] diff_mult_distrib[no_vars]}
 \rulename{diff_mult_distrib}
 
 @{thm[display] mod_mult_distrib[no_vars]}

 @{thm[display] zdiv_zmult2_eq[no_vars]}
 \rulename{zdiv_zmult2_eq}
 
 @{thm[display] zmod_zmult2_eq[no_vars]}
 \rulename{zmod_zmult2_eq}
-
-@{thm[display] abs_mult[no_vars]}
-\rulename{abs_mult}
 *}  
 
 lemma "abs (x+y) \<le> abs x + abs (y :: int)"
 by arith
 

 
 @{thm[display] int_less_induct[no_vars]}
 \rulename{int_less_induct}
 *}  
 
-text {*REALS
+text {*FIELDS
 
 @{thm[display] dense[no_vars]}
 \rulename{dense}
 
+@{thm[display] times_divide_eq_right[no_vars]}
+\rulename{times_divide_eq_right}
+
+@{thm[display] times_divide_eq_left[no_vars]}
+\rulename{times_divide_eq_left}
+
+@{thm[display] divide_divide_eq_right[no_vars]}
+\rulename{divide_divide_eq_right}
+
+@{thm[display] divide_divide_eq_left[no_vars]}
+\rulename{divide_divide_eq_left}
+
+@{thm[display] minus_divide_left[no_vars]}
+\rulename{minus_divide_left}
+
+@{thm[display] minus_divide_right[no_vars]}
+\rulename{minus_divide_right}
+
+This last NOT a simprule
+
+@{thm[display] add_divide_distrib[no_vars]}
+\rulename{add_divide_distrib}
+*}
+
+lemma "3/4 < (7/8 :: real)"
+by simp 
+
+lemma "P ((3/4) * (8/15 :: real))"
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+apply simp 
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+oops
+
+lemma "(3/4) * (8/15) < (x :: real)"
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+apply simp 
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+oops
+
+lemma "(3/4) * (10^15) < (x :: real)"
+apply simp 
+oops
+
+text{*
+Ring and Field
+
+Requires a field, or else an ordered ring
+
+@{thm[display] mult_eq_0_iff[no_vars]}
+\rulename{mult_eq_0_iff}
+
+@{thm[display] field_mult_eq_0_iff[no_vars]}
+\rulename{field_mult_eq_0_iff}
+
+@{thm[display] mult_cancel_right[no_vars]}
+\rulename{mult_cancel_right}
+
+@{thm[display] field_mult_cancel_right[no_vars]}
+\rulename{field_mult_cancel_right}
+*}
+
+ML{*set show_sorts*}
+
+text{*
+effect of show sorts on the above
+
+@{thm[display] field_mult_cancel_right[no_vars]}
+\rulename{field_mult_cancel_right}
+*}
+
+ML{*reset show_sorts*}
+
+
+text{*
+absolute value
+
+@{thm[display] abs_mult[no_vars]}
+\rulename{abs_mult}
+
+@{thm[display] abs_le_iff[no_vars]}
+\rulename{abs_le_iff}
+
+@{thm[display] abs_triangle_ineq[no_vars]}
+\rulename{abs_triangle_ineq}
+
+@{thm[display] power_add[no_vars]}
+\rulename{power_add}
+
+@{thm[display] power_mult[no_vars]}
+\rulename{power_mult}
+
 @{thm[display] power_abs[no_vars]}
 \rulename{power_abs}
 
-@{thm[display] times_divide_eq_right[no_vars]}
-\rulename{times_divide_eq_right}
-
-@{thm[display] times_divide_eq_left[no_vars]}
-\rulename{times_divide_eq_left}
-
-@{thm[display] divide_divide_eq_right[no_vars]}
-\rulename{divide_divide_eq_right}
-
-@{thm[display] divide_divide_eq_left[no_vars]}
-\rulename{divide_divide_eq_left}
-
-@{thm[display] minus_divide_left[no_vars]}
-\rulename{minus_divide_left}
-
-@{thm[display] minus_divide_right[no_vars]}
-\rulename{minus_divide_right}
-
-This last NOT a simprule
-
-@{thm[display] add_divide_distrib[no_vars]}
-\rulename{add_divide_distrib}
-*}
-
-lemma "3/4 < (7/8 :: real)"
-by simp 
-
-lemma "P ((3/4) * (8/15 :: real))"
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply simp 
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-oops
-
-lemma "(3/4) * (8/15) < (x :: real)"
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-apply simp 
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-*};
-oops
-
-lemma "(3/4) * (10^15) < (x :: real)"
-apply simp 
-oops
-
+
+*}
 
 
 end