# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260387352 -3600
# Node ID c636858377066d092379ef3898fc16b1250f9ba0
# Parent  2b35c7e90294b0781493d45a32333d35443a8d33
proved (with a lot of pain) that times_raw is respectful

diff -r 2b35c7e90294 -r c63685837706 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 17:31:19 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 20:35:52 2009 +0100
@@ -1,12 +1,11 @@
 theory IntEx2
-imports "../QuotMain"
+imports "../QuotMain" Nat Presburger
 (*uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
   ("Tools/int_arith.ML")*)
 begin
 
-
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
 where
@@ -81,9 +80,8 @@
 definition
   abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
 
-
 definition
-  sgn_int_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+  sgn_int_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
 
 instance ..
 
@@ -97,11 +95,40 @@
   shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
   by auto
 
+lemma times_raw_fst:
+  assumes a: "x \<approx> z"
+  shows "times_raw x y \<approx> times_raw z y"
+using a
+apply(cases x, cases y, cases z)
+apply(auto simp add: times_raw.simps intrel.simps)
+apply(rename_tac u v w x y z)
+apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+apply(simp add: mult_ac)
+apply(simp add: add_mult_distrib [symmetric])
+done
+
+lemma times_raw_snd:
+  assumes a: "x \<approx> z"
+  shows "times_raw y x \<approx> times_raw y z"
+using a
+apply(cases x, cases y, cases z)
+apply(auto simp add: times_raw.simps intrel.simps)
+apply(rename_tac u v w x y z)
+apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+apply(simp add: mult_ac)
+apply(simp add: add_mult_distrib [symmetric])
+done
+
 lemma mult_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"
-apply(auto)
-apply(simp add: algebra_simps)
-sorry
+apply(simp only: fun_rel.simps)
+apply(rule allI | rule impI)+
+apply(rule equivp_transp[OF int_equivp])
+apply(rule times_raw_fst)
+apply(assumption)
+apply(rule times_raw_snd)
+apply(assumption)
+done
 
 lemma less_eq_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw"
@@ -147,7 +174,6 @@
 
 text{*The integers form a @{text comm_ring_1}*}
 
-print_quotconsts
 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *}
 
 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *}
@@ -262,8 +288,7 @@
 proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
-    unfolding less_int_def
-    by (lifting test)
+    unfolding less_int_def by (lifting test)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: abs_int_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"