author Christian Urban Tue, 29 Jun 2010 02:18:08 +0100 changeset 37594 32ad67684ee7 parent 37593 2505feaf2d70 child 37608 165cd386288d
cosmetics: avoided statement of raw theorems, used the method descending instead
```--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Jun 29 01:38:29 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Jun 29 02:18:08 2010 +0100
@@ -114,43 +114,6 @@
apply(assumption)
done

-lemma plus_assoc_raw:
-  shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
-  by (cases i, cases j, cases k) (simp)
-
-lemma plus_sym_raw:
-  shows "plus_int_raw i j \<approx> plus_int_raw j i"
-  by (cases i, cases j) (simp)
-
-lemma plus_zero_raw:
-  shows "plus_int_raw (0, 0) i \<approx> i"
-  by (cases i) (simp)
-
-lemma plus_minus_zero_raw:
-  shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
-  by (cases i) (simp)
-
-lemma times_assoc_raw:
-  shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
-  by (cases i, cases j, cases k)
-     (simp add: algebra_simps)
-
-lemma times_sym_raw:
-  shows "times_int_raw i j \<approx> times_int_raw j i"
-  by (cases i, cases j) (simp add: algebra_simps)
-
-lemma times_one_raw:
-  shows "times_int_raw  (1, 0) i \<approx> i"
-  by (cases i) (simp)
-
-lemma times_plus_comm_raw:
-  shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
-by (cases i, cases j, cases k)
-   (simp add: 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}*}

@@ -158,25 +121,25 @@
proof
fix i j k :: int
show "(i + j) + k = i + (j + k)"
-    by (lifting plus_assoc_raw)
+    by (descending) (auto)
show "i + j = j + i"
-    by (lifting plus_sym_raw)
+    by (descending) (auto)
show "0 + i = (i::int)"
-    by (lifting plus_zero_raw)
+    by (descending) (auto)
show "- i + i = 0"
-    by (lifting plus_minus_zero_raw)
+    by (descending) (auto)
show "i - j = i + - j"
by (simp add: minus_int_def)
show "(i * j) * k = i * (j * k)"
-    by (lifting times_assoc_raw)
+    by (descending) (auto simp add: algebra_simps)
show "i * j = j * i"
-    by (lifting times_sym_raw)
+    by (descending) (auto)
show "1 * i = i"
-    by (lifting times_one_raw)
+    by (descending) (auto)
show "(i + j) * k = i * k + j * k"
-    by (lifting times_plus_comm_raw)
+    by (descending) (auto simp add: algebra_simps)
show "0 \<noteq> (1::int)"
-    by (lifting one_zero_distinct)
+    by (descending) (auto)
qed

lemma plus_int_raw_rsp_aux:
@@ -211,36 +174,19 @@
by (induct m)
(simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)

-lemma le_antisym_raw:
-  shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
-  by (cases i, cases j) (simp)
-
-lemma le_refl_raw:
-  shows "le_int_raw i i"
-  by (cases i) (simp)
-
-lemma le_trans_raw:
-  shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
-  by (cases i, cases j, cases k) (simp)
-
-lemma le_cases_raw:
-  shows "le_int_raw i j \<or> le_int_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"
-    by (lifting le_antisym_raw)
+    by (descending) (auto)
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
by (auto simp add: less_int_def dest: antisym)
show "i \<le> i"
-    by (lifting le_refl_raw)
+    by (descending) (auto)
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
-    by (lifting le_trans_raw)
+    by (descending) (auto)
show "i \<le> j \<or> j \<le> i"
-    by (lifting le_cases_raw)
+    by (descending) (auto)
qed

instantiation int :: distrib_lattice
@@ -258,15 +204,11 @@

end

-lemma le_plus_int_raw:
-  shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
-  by (cases i, cases j, cases k) (simp)
-
instance int :: ordered_cancel_ab_semigroup_add
proof
fix i j k :: int
show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-    by (lifting le_plus_int_raw)
+    by (descending) (auto)
qed

abbreviation
@@ -296,7 +238,7 @@
fixes k::int
shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
unfolding less_int_def int_of_nat
-  by (lifting zero_le_imp_eq_int_raw)
+  by (descending) (rule zero_le_imp_eq_int_raw)

lemma zmult_zless_mono2:
fixes i j k::int
@@ -365,16 +307,10 @@
shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
by (auto iff: int_to_nat_raw_def)

-lemma nat_le_eq_zle_raw:
-  assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
-  shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
-  using a
-  by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
-
lemma nat_le_eq_zle:
fixes w z::"int"
shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
unfolding less_int_def
-  by (lifting nat_le_eq_zle_raw)
+  by (descending) (auto simp add: int_to_nat_raw_def)

end```
```--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 01:38:29 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 02:18:08 2010 +0100
@@ -32,7 +32,7 @@
text{*Proving that it is an equivalence relation*}

lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
+by (induct X) (auto intro: msgrel.intros)

theorem equiv_msgrel: "equivp msgrel"
proof (rule equivpI)
@@ -263,68 +263,47 @@

subsection{*Injectivity Properties of Some Constructors*}

-lemma NONCE_imp_eq:
-  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
-  by (drule msgrel_imp_eq_freenonces, simp)
-
text{*Can also be proved using the function @{term nonces}*}
lemma Nonce_Nonce_eq [iff]:
shows "(Nonce m = Nonce n) = (m = n)"
proof
assume "Nonce m = Nonce n"
-  then show "m = n" by (lifting NONCE_imp_eq)
+  then show "m = n"
+    by (descending) (drule msgrel_imp_eq_freenonces, simp)
next
assume "m = n"
then show "Nonce m = Nonce n" by simp
qed

-lemma MPAIR_imp_eqv_left:
-  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
-  by (drule msgrel_imp_eqv_freeleft) (simp)
-
lemma MPair_imp_eq_left:
assumes eq: "MPair X Y = MPair X' Y'"
shows "X = X'"
-  using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
-  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
-  by (drule msgrel_imp_eqv_freeright) (simp)
+  using eq
+  by (descending) (drule msgrel_imp_eqv_freeleft, simp)

lemma MPair_imp_eq_right:
shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
-  by (lifting  MPAIR_imp_eqv_right)
+  by (descending) (drule msgrel_imp_eqv_freeright, simp)

theorem MPair_MPair_eq [iff]:
shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

-lemma NONCE_neqv_MPAIR:
-  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
-  by (auto dest: msgrel_imp_eq_freediscrim)
-
theorem Nonce_neq_MPair [iff]:
shows "Nonce N \<noteq> MPair X Y"
-  by (lifting NONCE_neqv_MPAIR)
+  by (descending) (auto dest: msgrel_imp_eq_freediscrim)

text{*Example suggested by a referee*}

-lemma CRYPT_NONCE_neq_NONCE:
-  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
-  by (auto dest: msgrel_imp_eq_freediscrim)
-
theorem Crypt_Nonce_neq_Nonce:
shows "Crypt K (Nonce M) \<noteq> Nonce N"
-  by (lifting CRYPT_NONCE_neq_NONCE)
+  by (descending) (auto dest: msgrel_imp_eq_freediscrim)

text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
-  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
-  by (auto dest: msgrel_imp_eq_freediscrim)

theorem Crypt2_Nonce_neq_Nonce:
shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
-  by (lifting CRYPT2_NONCE_neq_NONCE)
+  by (descending) (auto dest: msgrel_imp_eq_freediscrim)

theorem Crypt_Crypt_eq [iff]:
shows "(Crypt K X = Crypt K X') = (X=X')"```