# HG changeset patch # User Cezary Kaliszyk # Date 1260136623 -3600 # Node ID eac2662a21ec8cccb29021aafef858223fb001a9 # Parent 334b3e9ea3e01f0b03b8aec06571f0ae09f6e77b Solved all quotient goals. diff -r 334b3e9ea3e0 -r eac2662a21ec IntEx2.thy --- a/IntEx2.thy Sun Dec 06 06:58:24 2009 +0100 +++ b/IntEx2.thy Sun Dec 06 22:57:03 2009 +0100 @@ -53,7 +53,7 @@ where "minus_raw (x, y) = (y, x)" -quotient_def +quotient_def minus_qnt::"int \ int" where "minus_qnt \ minus_raw" @@ -110,6 +110,10 @@ shows "(op \ ===> op \ ===> op \) plus_raw plus_raw" by auto +lemma minus_raw_rsp[quotient_rsp]: + shows "(op \ ===> op \) minus_raw minus_raw" + by auto + lemma mult_raw_rsp[quotient_rsp]: shows "(op \ ===> op \ ===> op \) mult_raw mult_raw" apply(auto) @@ -155,9 +159,9 @@ (simp add: mult algebra_simps) lemma one_zero_distinct: - shows "(0, 0) \ ((1::nat), (0::nat))" + shows "\ (0, 0) \ ((1::nat), (0::nat))" by simp - + text{*The integers form a @{text comm_ring_1}*} @@ -178,61 +182,34 @@ done show "0 + i = (i::int)" unfolding add_int_def Zero_int_def - apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *}) + done show "- i + i = 0" unfolding add_int_def minus_int_def Zero_int_def - apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 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 {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *}) + done show "i * j = j * i" unfolding mult_int_def - apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *}) + done show "1 * i = i" unfolding mult_int_def One_int_def - apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *}) + done show "(i + j) * k = i * k + j * k" unfolding mult_int_def add_int_def - apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *}) - apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *}) + done show "0 \ (1::int)" unfolding Zero_int_def One_int_def - apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *}) - defer - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *}) + done qed term of_nat @@ -316,8 +293,8 @@ qed lemma test: - "\le_raw i j \ i \ j; le_raw (0, 0) k \ (0, 0) \ k\ - \ le_raw (mult_raw k i) (mult_raw k j) \ mult_raw k i \ mult_raw k j" + "\le_raw i j \ \i \ j; le_raw (0, 0) k \ \(0, 0) \ k\ + \ le_raw (mult_raw k i) (mult_raw k j) \ \mult_raw k i \ mult_raw k j" apply(cases i, cases j, cases k) apply(auto simp add: mult algebra_simps) sorry @@ -329,12 +306,8 @@ fix i j k :: int show "i < j \ 0 < k \ k * i < k * j" unfolding mult_int_def le_int_def less_int_def Zero_int_def - apply(tactic {* procedure_tac @{context} @{thm test} 1 *}) - defer - apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) - defer - apply(tactic {* clean_tac @{context} 1*}) - sorry + apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *}) + done show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) show "sgn (i\int) = (if i=0 then 0 else if 0