# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260527152 -3600
# Node ID add8f7f311cd5603cb3659d85cff405f5041838a
# Parent  596467882518e9f22894d13cbee093eff8efe0c5
Renamed theorems in IntEx2 to conform to names in Int.

diff -r 596467882518 -r add8f7f311cd Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 11:19:41 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 11:25:52 2009 +0100
@@ -46,21 +46,20 @@
   minus_int_def [code del]:  "z - w = z + (-w::int)"
 
 fun
-  times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
-  "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_def
-  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "times_raw"
+  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
 
-(* PROBLEM: this should be called le_int and le_raw / or odd *)
 fun
-  less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
-  "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
+  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_def
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "less_eq_raw"
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -83,43 +82,43 @@
   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
   by auto
 
-lemma times_raw_fst:
+lemma mult_raw_fst:
   assumes a: "x \<approx> z"
-  shows "times_raw x y \<approx> times_raw z y"
+  shows "mult_raw x y \<approx> mult_raw z y"
 using a
 apply(cases x, cases y, cases z)
-apply(auto simp add: times_raw.simps intrel.simps)
+apply(auto simp add: mult_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:
+lemma mult_raw_snd:
   assumes a: "x \<approx> z"
-  shows "times_raw y x \<approx> times_raw y z"
+  shows "mult_raw y x \<approx> mult_raw y z"
 using a
 apply(cases x, cases y, cases z)
-apply(auto simp add: times_raw.simps intrel.simps)
+apply(auto simp add: mult_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_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"
+lemma mult_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 apply(simp only: fun_rel.simps)
 apply(rule allI | rule impI)+
 apply(rule equivp_transp[OF int_equivp])
-apply(rule times_raw_fst)
+apply(rule mult_raw_fst)
 apply(assumption)
-apply(rule times_raw_snd)
+apply(rule mult_raw_snd)
 apply(assumption)
 done
 
-lemma less_eq_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw"
+lemma le_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
 by auto
 
 lemma plus_assoc_raw:
@@ -139,20 +138,20 @@
 by (cases i) (simp)
 
 lemma times_assoc_raw:
-  shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)"
+  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
 by (cases i, cases j, cases k) 
    (simp add: algebra_simps)
 
 lemma times_sym_raw:
-  shows "times_raw i j \<approx> times_raw j i"
+  shows "mult_raw i j \<approx> mult_raw j i"
 by (cases i, cases j) (simp add: algebra_simps)
 
 lemma times_one_raw:
-  shows "times_raw  (1, 0) i \<approx> i"
+  shows "mult_raw  (1, 0) i \<approx> i"
 by (cases i) (simp)
 
 lemma times_plus_comm_raw:
-  shows "times_raw (plus_raw i j) k \<approx> plus_raw (times_raw i k) (times_raw j k)"
+  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 by (cases i, cases j, cases k) 
    (simp add: algebra_simps)
 
@@ -221,19 +220,19 @@
 done
 
 lemma le_antisym_raw:
-  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
+  shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
 by (cases i, cases j) (simp)
 
 lemma le_refl_raw:
-  shows "less_eq_raw i i"
+  shows "le_raw i i"
 by (cases i) (simp)
 
 lemma le_trans_raw:
-  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j k \<Longrightarrow> less_eq_raw i k"
+  shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
 by (cases i, cases j, cases k) (simp)
 
 lemma le_cases_raw:
-  shows "less_eq_raw i j \<or> less_eq_raw j i"
+  shows "le_raw i j \<or> le_raw j i"
 by (cases i, cases j) 
    (simp add: linorder_linear)
 
@@ -268,7 +267,7 @@
 end
 
 lemma le_plus_raw:
-  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw (plus_raw k i) (plus_raw k j)"
+  shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
 by (cases i, cases j, cases k) (simp)
 
 
@@ -280,7 +279,7 @@
 qed
 
 abbreviation
-  "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"
+  "less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"
 
 lemma zmult_zless_mono2_lemma:
   fixes i j::int