# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260527549 -3600
# Node ID 09c192b61100a483852b651f0250a577e65bf797
# Parent  810d59a3d9b08203dedc12c55aadde1bd42227a3# Parent  587e97d144a0cbbb7ffc5e6bf8ab721709aeb8bf
Merge

diff -r 587e97d144a0 -r 09c192b61100 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 11:14:05 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 11:32:29 2009 +0100
@@ -18,13 +18,13 @@
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
-ML {* @{term "0 :: int"} *}
+ML {* @{term "0 \<Colon> int"} *}
 
 quotient_def
-  "0 :: int" as "(0::nat, 0::nat)"
+  "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
 
 quotient_def
-  "1 :: int" as "(1::nat, 0::nat)"
+  "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -32,7 +32,7 @@
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_def
-  "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
 
 fun
   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -40,36 +40,35 @@
   "uminus_raw (x, y) = (y, x)"
 
 quotient_def
-  "(uminus :: (int \<Rightarrow> int))" as "uminus_raw"
+  "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
 
 definition
-  minus_int_def [code del]:  "z - w = z + (-w::int)"
+  minus_int_def [code del]:  "z - w = z + (-w\<Colon>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)"
 
 definition
-  abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+  zabs_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)"
+  zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
 
 instance ..
 
@@ -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
@@ -325,16 +324,16 @@
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
-    by (simp only: abs_int_def)
+    by (simp only: zabs_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-    by (simp only: sgn_int_def)
+    by (simp only: zsgn_def)
 qed
 
 instance int :: lordered_ring
 proof  
   fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
 qed
 
 lemmas int_distrib =
diff -r 587e97d144a0 -r 09c192b61100 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Dec 11 11:14:05 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 11 11:32:29 2009 +0100
@@ -3,7 +3,7 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
-  val make_def: mixfix -> Attrib.binding -> term -> term ->
+  val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
@@ -76,7 +76,15 @@
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")
 
-fun make_def mx attr lhs rhs lthy =
+(* interface and syntax setup *)
+
+(* the ML-interface takes a 4-tuple consisting of *)
+(*                                                *)
+(* - the mixfix annotation                        *)
+(* - name and attributes of the meta eq           *)
+(* - the new constant including its type          *)
+(* - the rhs of the definition                    *)
+fun quotient_def mx attr lhs rhs lthy =
 let
   val Free (lhs_str, lhs_ty) = lhs;
   val qconst_bname = Binding.name lhs_str;
@@ -95,22 +103,12 @@
   ((trm, thm), lthy'')
 end
 
-(* interface and syntax setup *)
-
-(* the ML-interface takes a 5-tuple consisting of  *)
-(*                                                 *)
-(* - the name of the constant to be lifted         *)
-(* - its type                                      *)
-(* - its mixfix annotation                         *)
-(* - a meta-equation defining the constant,        *)
-(*   and the attributes of for this meta-equality  *)
-
-fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = 
+fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =
 let
   val lhs = Syntax.read_term lthy lhsstr
   val rhs = Syntax.read_term lthy rhsstr
 in
-  make_def mx attr lhs rhs lthy |> snd
+  quotient_def mx attr lhs rhs lthy |> snd
 end
 
 val _ = OuterKeyword.keyword "as";