--- a/IntEx2.thy Mon Dec 07 14:00:36 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,436 +0,0 @@
-theory IntEx2
-imports QuotMain
-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
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient int = "nat \<times> nat" / intrel
- apply(unfold equivp_def)
- apply(auto simp add: mem_def expand_fun_eq)
- done
-
-instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
-begin
-
-quotient_def
- zero_qnt::"int"
-where
- "zero_qnt \<equiv> (0::nat, 0::nat)"
-
-definition Zero_int_def[code del]:
- "0 = zero_qnt"
-
-quotient_def
- one_qnt::"int"
-where
- "one_qnt \<equiv> (1::nat, 0::nat)"
-
-definition One_int_def[code del]:
- "1 = one_qnt"
-
-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"
-where
- "plus_qnt \<equiv> plus_raw"
-
-definition add_int_def[code del]:
- "z + w = plus_qnt z w"
-
-fun
- minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
- "minus_raw (x, y) = (y, x)"
-
-quotient_def
- minus_qnt::"int \<Rightarrow> int"
-where
- "minus_qnt \<equiv> minus_raw"
-
-definition minus_int_def [code del]:
- "- z = minus_qnt z"
-
-definition
- diff_int_def [code del]: "z - w = z + (-w::int)"
-
-fun
- mult_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)"
-
-quotient_def
- mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
-where
- "mult_qnt \<equiv> mult_raw"
-
-definition
- mult_int_def [code del]: "z * w = mult_qnt z w"
-
-fun
- le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
- "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
-
-quotient_def
- le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
-where
- "le_qnt \<equiv> le_raw"
-
-definition
- le_int_def [code del]:
- "z \<le> w = le_qnt z w"
-
-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)"
-
-definition
- zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-
-instance ..
-
-end
-
-thm add_assoc
-
-lemma plus_raw_rsp[quotient_rsp]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
-by auto
-
-lemma minus_raw_rsp[quotient_rsp]:
- shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
- by auto
-
-lemma mult_raw_rsp[quotient_rsp]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-apply(auto)
-apply(simp add: mult algebra_simps)
-sorry
-
-lemma le_raw_rsp[quotient_rsp]:
- shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
-by auto
-
-lemma plus_assoc_raw:
- shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
-by (cases i, cases j, cases k) (simp)
-
-lemma plus_sym_raw:
- shows "plus_raw i j \<approx> plus_raw j i"
-by (cases i, cases j) (simp)
-
-lemma plus_zero_raw:
- shows "plus_raw (0, 0) i \<approx> i"
-by (cases i) (simp)
-
-lemma plus_minus_zero_raw:
- 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)"
-by (cases i, cases j, cases k)
- (simp add: mult algebra_simps)
-
-lemma mult_sym_raw:
- shows "mult_raw i j \<approx> mult_raw j i"
-by (cases i, cases j) (simp)
-
-lemma mult_one_raw:
- shows "mult_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)"
-by (cases i, cases j, cases k)
- (simp add: mult algebra_simps)
-
-lemma one_zero_distinct:
- shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
- by simp
-
-text{*The integers form a @{text comm_ring_1}*}
-
-
-ML {* val qty = @{typ "int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
-
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)"
- unfolding add_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})
- done
- show "i + j = j + i"
- unfolding add_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
- done
- show "0 + i = (i::int)"
- unfolding add_int_def Zero_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *})
- done
- show "- i + i = 0"
- unfolding add_int_def minus_int_def Zero_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *})
- done
- show "i - j = i + - j"
- by (simp add: diff_int_def)
- show "(i * j) * k = i * (j * k)"
- unfolding mult_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *})
- done
- show "i * j = j * i"
- unfolding mult_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *})
- done
- show "1 * i = i"
- unfolding mult_int_def One_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *})
- done
- show "(i + j) * k = i * k + j * k"
- unfolding mult_int_def add_int_def
- apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *})
- done
- show "0 \<noteq> (1::int)"
- unfolding Zero_int_def One_int_def
- apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *})
- done
-qed
-
-term of_nat
-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(simp)
-apply(simp add: add_int_def One_int_def)
-apply(simp add: plus_qnt_def one_qnt_def)
-oops
-
-lemma le_antisym_raw:
- 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 "le_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"
-by (cases i, cases j, cases k) (simp)
-
-lemma le_cases_raw:
- shows "le_raw i j \<or> le_raw j i"
-by (cases i, cases j)
- (simp add: linorder_linear)
-
-instance int :: linorder
-proof
- fix i j k :: int
- show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
- unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})
- done
- 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
- apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})
- done
- show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
- unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})
- done
- show "i \<le> j \<or> j \<le> i"
- unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
- done
-qed
-
-instantiation int :: distrib_lattice
-begin
-
-definition
- "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
-
-definition
- "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
-
-instance
- by intro_classes
- (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
-
-end
-
-lemma le_plus_raw:
- shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
-by (cases i, cases j, cases k) (simp)
-
-
-instance int :: pordered_cancel_ab_semigroup_add
-proof
- fix i j k :: int
- show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- unfolding le_int_def add_int_def
- apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})
- done
-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"
-apply(cases i, cases j, cases k)
-apply(auto simp add: mult algebra_simps)
-sorry
-
-
-text{*The integers form an ordered integral domain*}
-instance int :: ordered_idom
-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
- apply(tactic {* lift_tac @{context} @{thm test} 1 *})
- done
- show "\<bar>i\<bar> = (if i < 0 then -i else i)"
- 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: zsgn_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])
-qed
-
-lemmas int_distrib =
- left_distrib [of "z1::int" "z2" "w", standard]
- right_distrib [of "w::int" "z1" "z2", standard]
- left_diff_distrib [of "z1::int" "z2" "w", standard]
- right_diff_distrib [of "w::int" "z1" "z2", standard]
-
-
-subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
-
-(*
-context ring_1
-begin
-
-
-definition
- of_int :: "int \<Rightarrow> 'a"
-where
- "of_int
-*)
-
-
-subsection {* Binary representation *}
-
-text {*
- This formalization defines binary arithmetic in terms of the integers
- rather than using a datatype. This avoids multiple representations (leading
- zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text
- int_of_binary}, for the numerical interpretation.
-
- The representation expects that @{text "(m mod 2)"} is 0 or 1,
- even if m is negative;
- For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
- @{text "-5 = (-3)*2 + 1"}.
-
- This two's complement binary representation derives from the paper
- "An Efficient Representation of Arithmetic for Term Rewriting" by
- Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
- Springer LNCS 488 (240-251), 1991.
-*}
-
-subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
-
-definition
- Pls :: int where
- [code del]: "Pls = 0"
-
-definition
- Min :: int where
- [code del]: "Min = - 1"
-
-definition
- Bit0 :: "int \<Rightarrow> int" where
- [code del]: "Bit0 k = k + k"
-
-definition
- Bit1 :: "int \<Rightarrow> int" where
- [code del]: "Bit1 k = 1 + k + k"
-
-class number = -- {* for numeric types: nat, int, real, \dots *}
- fixes number_of :: "int \<Rightarrow> 'a"
-
-use "~~/src/HOL/Tools/numeral.ML"
-
-syntax
- "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
-
-use "~~/src/HOL/Tools/numeral_syntax.ML"
-(*
-setup NumeralSyntax.setup
-
-abbreviation
- "Numeral0 \<equiv> number_of Pls"
-
-abbreviation
- "Numeral1 \<equiv> number_of (Bit1 Pls)"
-
-lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
- -- {* Unfold all @{text let}s involving constants *}
- unfolding Let_def ..
-
-definition
- succ :: "int \<Rightarrow> int" where
- [code del]: "succ k = k + 1"
-
-definition
- pred :: "int \<Rightarrow> int" where
- [code del]: "pred k = k - 1"
-
-lemmas
- max_number_of [simp] = max_def
- [of "number_of u" "number_of v", standard, simp]
-and
- min_number_of [simp] = min_def
- [of "number_of u" "number_of v", standard, simp]
- -- {* unfolding @{text minx} and @{text max} on numerals *}
-
-lemmas numeral_simps =
- succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
-
-text {* Removal of leading zeroes *}
-
-lemma Bit0_Pls [simp, code_post]:
- "Bit0 Pls = Pls"
- unfolding numeral_simps by simp
-
-lemma Bit1_Min [simp, code_post]:
- "Bit1 Min = Min"
- unfolding numeral_simps by simp
-
-lemmas normalize_bin_simps =
- Bit0_Pls Bit1_Min
-*)
\ No newline at end of file