diff -r 2d9de77d5687 -r 0dd10a900cae Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -20,34 +20,27 @@
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
-quotient_def 
-  zero_qnt::"int"
+quotient_def
+  zero_int::"0 :: int"
 where
-  "zero_qnt \<equiv> (0::nat, 0::nat)"
-
-definition  Zero_int_def[code del]: 
-  "0 = zero_qnt"
+  "(0::nat, 0::nat)"
 
-quotient_def 
-  one_qnt::"int"
+thm zero_int_def
+
+quotient_def
+  one_int::"1 :: int"
 where
-  "one_qnt \<equiv> (1::nat, 0::nat)"
-
-definition One_int_def[code del]:
-  "1 = one_qnt"
+  "(1::nat, 0::nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def 
-  plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+quotient_def
+  plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)"
 where
-  "plus_qnt \<equiv> plus_raw"
-
-definition add_int_def[code del]:
-  "z + w = plus_qnt z w"
+  "plus_raw"
 
 fun
   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -55,51 +48,42 @@
   "minus_raw (x, y) = (y, x)"
 
 quotient_def
-  minus_qnt::"int \<Rightarrow> int"
+  uminus_int::"(uminus :: (int \<Rightarrow> int))"
 where
-  "minus_qnt \<equiv> minus_raw"
-
-definition minus_int_def [code del]:
-    "- z = minus_qnt z"
+  "minus_raw"
 
 definition
-  diff_int_def [code del]:  "z - w = z + (-w::int)"
+  minus_int_def [code del]:  "z - w = z + (-w::int)"
 
 fun
-  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+  times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
-  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+  "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def 
-  mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+quotient_def
+  times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)"
 where
-  "mult_qnt \<equiv> mult_raw"
-
-definition
-  mult_int_def [code del]: "z * w = mult_qnt z w"
+  "times_raw"
 
 fun
-  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+  less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
-  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
+  "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def 
-  le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
+quotient_def
+  less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
 where
-  "le_qnt \<equiv> le_raw"
-
-definition
-  le_int_def [code del]:
-   "z \<le> w = le_qnt z w"
+  "less_eq_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
 
 definition
-  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+  abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
 
 definition
-  zsgn_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 ..
 
@@ -114,13 +98,13 @@
   by auto
 
 lemma mult_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"
 apply(auto)
 apply(simp add: algebra_simps)
 sorry
 
-lemma le_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
+lemma less_eq_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw"
 by auto
 
 lemma plus_assoc_raw:
@@ -139,21 +123,21 @@
   shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
 by (cases i) (simp)
 
-lemma mult_assoc_raw:
-  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
+lemma times_assoc_raw:
+  shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)"
 by (cases i, cases j, cases k) 
    (simp add: algebra_simps)
 
-lemma mult_sym_raw:
-  shows "mult_raw i j \<approx> mult_raw j i"
+lemma times_sym_raw:
+  shows "times_raw i j \<approx> times_raw j i"
 by (cases i, cases j) (simp add: algebra_simps)
 
-lemma mult_one_raw:
-  shows "mult_raw  (1, 0) i \<approx> i"
+lemma times_one_raw:
+  shows "times_raw  (1, 0) i \<approx> i"
 by (cases i) (simp)
 
-lemma mult_plus_comm_raw:
-  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
+lemma times_plus_comm_raw:
+  shows "times_raw (plus_raw i j) k \<approx> plus_raw (times_raw i k) (times_raw j k)"
 by (cases i, cases j, cases k) 
    (simp add: algebra_simps)
 
@@ -163,38 +147,36 @@
 
 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"})) *}
+ML {* @{term "0 :: int"} *}
+
+thm plus_assoc_raw
 
 instance int :: comm_ring_1
 proof
   fix i j k :: int
   show "(i + j) + k = i + (j + k)"
-    unfolding add_int_def
-    by (lifting plus_assoc_raw)
+     by (lifting plus_assoc_raw)
   show "i + j = j + i" 
-    unfolding add_int_def
     by (lifting plus_sym_raw)
   show "0 + i = (i::int)"
-    unfolding add_int_def Zero_int_def 
     by (lifting plus_zero_raw)
   show "- i + i = 0"
-    unfolding add_int_def minus_int_def Zero_int_def 
     by (lifting plus_minus_zero_raw)
   show "i - j = i + - j"
-    by (simp add: diff_int_def)
+    by (simp add: minus_int_def)
   show "(i * j) * k = i * (j * k)"
-    unfolding mult_int_def 
-    by (lifting mult_assoc_raw)
+    by (lifting times_assoc_raw)
   show "i * j = j * i"
-    unfolding mult_int_def 
-    by (lifting mult_sym_raw)
+    by (lifting times_sym_raw)
   show "1 * i = i"
-    unfolding mult_int_def One_int_def
-    by (lifting mult_one_raw)
+    by (lifting times_one_raw)
   show "(i + j) * k = i * k + j * k"
-    unfolding mult_int_def add_int_def
-    by (lifting mult_plus_comm_raw)
+    by (lifting times_plus_comm_raw)
   show "0 \<noteq> (1::int)"
-    unfolding Zero_int_def One_int_def
     by (lifting one_zero_distinct)
 qed
 
@@ -202,27 +184,26 @@
 thm of_nat_def
 
 lemma int_def: "of_nat m = ABS_int (m, 0)"
-apply(induct m) 
-apply(simp add: Zero_int_def zero_qnt_def)
+apply(induct m)
+apply(simp add: zero_int_def)
 apply(simp)
-apply(simp add: add_int_def One_int_def)
-apply(simp add: plus_qnt_def one_qnt_def)
+apply(simp add: plus_int_def one_int_def)
 oops
 
 lemma le_antisym_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
+  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
 by (cases i, cases j) (simp)
 
 lemma le_refl_raw:
-  shows "le_raw i i"
+  shows "less_eq_raw i i"
 by (cases i) (simp)
 
 lemma le_trans_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
+  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j k \<Longrightarrow> less_eq_raw i k"
 by (cases i, cases j, cases k) (simp)
 
 lemma le_cases_raw:
-  shows "le_raw i j \<or> le_raw j i"
+  shows "less_eq_raw i j \<or> less_eq_raw j i"
 by (cases i, cases j) 
    (simp add: linorder_linear)
 
@@ -230,18 +211,14 @@
 proof
   fix i j k :: int
   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
-    unfolding le_int_def
     by (lifting le_antisym_raw)
   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
     by (auto simp add: less_int_def dest: antisym) 
   show "i \<le> i"
-    unfolding le_int_def
     by (lifting le_refl_raw)
   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
-    unfolding le_int_def
     by (lifting le_trans_raw)
   show "i \<le> j \<or> j \<le> i"
-    unfolding le_int_def
     by (lifting le_cases_raw)
 qed
 
@@ -261,7 +238,7 @@
 end
 
 lemma le_plus_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
+  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw (plus_raw k i) (plus_raw k j)"
 by (cases i, cases j, cases k) (simp)
 
 
@@ -269,13 +246,12 @@
 proof
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-    unfolding le_int_def add_int_def
     by (lifting le_plus_raw)
 qed
 
 lemma test:
-  "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
-    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
+  "\<lbrakk>less_eq_raw i j \<and> \<not>i \<approx> j; less_eq_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
+    \<Longrightarrow> less_eq_raw (times_raw k i) (times_raw k j) \<and> \<not>times_raw k i \<approx> times_raw k j"
 apply(cases i, cases j, cases k)
 apply(auto simp add: algebra_simps)
 sorry
@@ -286,19 +262,19 @@
 proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
-    unfolding mult_int_def le_int_def less_int_def Zero_int_def
+    unfolding less_int_def
     by (lifting test)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
-    by (simp only: zabs_def)
+    by (simp only: abs_int_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-    by (simp only: zsgn_def)
+    by (simp only: sgn_int_def)
 qed
 
 instance int :: lordered_ring
 proof  
   fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric])
 qed
 
 lemmas int_distrib =
@@ -414,4 +390,4 @@
   Bit0_Pls Bit1_Min
 *)
 
-end
\ No newline at end of file
+end