src/HOL/ex/BinEx.ML

Unary minus is now #- and not #~

(*** Examples of performing binary arithmetic by simplification ***)

(** Addition **)

Goal "#13  +  #19 = #32";
by (Simp_tac 1);
result();

Goal "#1234  +  #5678 = #6912";
by (Simp_tac 1);
result();

Goal "#1359  +  #-2468 = #-1109";
by (Simp_tac 1);
result();

Goal "#93746 +  #-46375 = #47371";
by (Simp_tac 1);
result();

(** Negation **)

Goal "- #65745 = #-65745";
by (Simp_tac 1);
result();

Goal "- #-54321 = #54321";
by (Simp_tac 1);
result();


(** Multiplication **)

Goal "#13  *  #19 = #247";
by (Simp_tac 1);
result();

Goal "#-84  *  #51 = #-4284";
by (Simp_tac 1);
result();

Goal "#255  *  #255 = #65025";
by (Simp_tac 1);
result();

Goal "#1359  *  #-2468 = #-3354012";
by (Simp_tac 1);
result();

Goal "#89 * #10 ~= #889";  
by (Simp_tac 1); 
result();

Goal "#13 < #18 - #4";  
by (Simp_tac 1); 
result();

Goal "#-345 < #-242 + #-100";  
by (Simp_tac 1); 
result();

Goal "#13557456 < #18678654";  
by (Simp_tac 1); 
result();

Goal "#999999 <= (#1000001 + #1)-#2";  
by (Simp_tac 1); 
result();

Goal "#1234567 <= #1234567";  
by (Simp_tac 1); 
result();