# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277774288 -3600
# Node ID 32ad67684ee77265ce02ec24d83ff88d94563e71
# Parent  2505feaf2d70f0f4df5b3639a2c7334f0751c7b1
cosmetics: avoided statement of raw theorems, used the method descending instead

diff -r 2505feaf2d70 -r 32ad67684ee7 src/HOL/Quotient_Examples/Quotient_Int.thy
--- 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
diff -r 2505feaf2d70 -r 32ad67684ee7 src/HOL/Quotient_Examples/Quotient_Message.thy
--- 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')"