--- a/IntEx2.thy Sun Dec 06 23:32:27 2009 +0100
+++ b/IntEx2.thy Sun Dec 06 23:35:02 2009 +0100
@@ -54,7 +54,7 @@
where
"minus_raw (x, y) = (y, x)"
-quotient_def
+quotient_def
minus_qnt::"int \<Rightarrow> int"
where
"minus_qnt \<equiv> minus_raw"
@@ -111,6 +111,10 @@
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)
@@ -156,9 +160,9 @@
(simp add: mult algebra_simps)
lemma one_zero_distinct:
- shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
+ shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
by simp
-
+
text{*The integers form a @{text comm_ring_1}*}
@@ -171,69 +175,42 @@
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 *})
+ apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
done
show "i + j = j + i"
unfolding add_int_def
- apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
+ apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
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} 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} 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} 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} 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} 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} 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 \<noteq> (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
@@ -269,21 +246,21 @@
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 *})
+ apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 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 *})
+ apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 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 *})
+ apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
done
show "i \<le> j \<or> j \<le> i"
unfolding le_int_def
- apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
+ apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
done
qed
@@ -312,13 +289,13 @@
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 *})
+ apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
done
qed
lemma test:
- "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
- \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
+ "\<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
@@ -330,12 +307,8 @@
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 {* 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 "\<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)"