--- 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