cosmetics: avoided statement of raw theorems, used the method descending instead
authorChristian Urban <urbanc@in.tum.de>
Tue Jun 29 02:18:08 2010 +0100 (2010-06-29)
changeset 3759432ad67684ee7
parent 37593 2505feaf2d70
child 37608 165cd386288d
cosmetics: avoided statement of raw theorems, used the method descending instead
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Jun 29 01:38:29 2010 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Jun 29 02:18:08 2010 +0100
     1.3 @@ -114,43 +114,6 @@
     1.4    apply(assumption)
     1.5    done
     1.6  
     1.7 -lemma plus_assoc_raw:
     1.8 -  shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
     1.9 -  by (cases i, cases j, cases k) (simp)
    1.10 -
    1.11 -lemma plus_sym_raw:
    1.12 -  shows "plus_int_raw i j \<approx> plus_int_raw j i"
    1.13 -  by (cases i, cases j) (simp)
    1.14 -
    1.15 -lemma plus_zero_raw:
    1.16 -  shows "plus_int_raw (0, 0) i \<approx> i"
    1.17 -  by (cases i) (simp)
    1.18 -
    1.19 -lemma plus_minus_zero_raw:
    1.20 -  shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
    1.21 -  by (cases i) (simp)
    1.22 -
    1.23 -lemma times_assoc_raw:
    1.24 -  shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
    1.25 -  by (cases i, cases j, cases k)
    1.26 -     (simp add: algebra_simps)
    1.27 -
    1.28 -lemma times_sym_raw:
    1.29 -  shows "times_int_raw i j \<approx> times_int_raw j i"
    1.30 -  by (cases i, cases j) (simp add: algebra_simps)
    1.31 -
    1.32 -lemma times_one_raw:
    1.33 -  shows "times_int_raw  (1, 0) i \<approx> i"
    1.34 -  by (cases i) (simp)
    1.35 -
    1.36 -lemma times_plus_comm_raw:
    1.37 -  shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
    1.38 -by (cases i, cases j, cases k)
    1.39 -   (simp add: algebra_simps)
    1.40 -
    1.41 -lemma one_zero_distinct:
    1.42 -  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
    1.43 -  by simp
    1.44  
    1.45  text{* The integers form a @{text comm_ring_1}*}
    1.46  
    1.47 @@ -158,25 +121,25 @@
    1.48  proof
    1.49    fix i j k :: int
    1.50    show "(i + j) + k = i + (j + k)"
    1.51 -    by (lifting plus_assoc_raw)
    1.52 +    by (descending) (auto)
    1.53    show "i + j = j + i"
    1.54 -    by (lifting plus_sym_raw)
    1.55 +    by (descending) (auto)
    1.56    show "0 + i = (i::int)"
    1.57 -    by (lifting plus_zero_raw)
    1.58 +    by (descending) (auto)
    1.59    show "- i + i = 0"
    1.60 -    by (lifting plus_minus_zero_raw)
    1.61 +    by (descending) (auto)
    1.62    show "i - j = i + - j"
    1.63      by (simp add: minus_int_def)
    1.64    show "(i * j) * k = i * (j * k)"
    1.65 -    by (lifting times_assoc_raw)
    1.66 +    by (descending) (auto simp add: algebra_simps)
    1.67    show "i * j = j * i"
    1.68 -    by (lifting times_sym_raw)
    1.69 +    by (descending) (auto)
    1.70    show "1 * i = i"
    1.71 -    by (lifting times_one_raw)
    1.72 +    by (descending) (auto)
    1.73    show "(i + j) * k = i * k + j * k"
    1.74 -    by (lifting times_plus_comm_raw)
    1.75 +    by (descending) (auto simp add: algebra_simps)
    1.76    show "0 \<noteq> (1::int)"
    1.77 -    by (lifting one_zero_distinct)
    1.78 +    by (descending) (auto)
    1.79  qed
    1.80  
    1.81  lemma plus_int_raw_rsp_aux:
    1.82 @@ -211,36 +174,19 @@
    1.83    by (induct m)
    1.84       (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
    1.85  
    1.86 -lemma le_antisym_raw:
    1.87 -  shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
    1.88 -  by (cases i, cases j) (simp)
    1.89 -
    1.90 -lemma le_refl_raw:
    1.91 -  shows "le_int_raw i i"
    1.92 -  by (cases i) (simp)
    1.93 -
    1.94 -lemma le_trans_raw:
    1.95 -  shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
    1.96 -  by (cases i, cases j, cases k) (simp)
    1.97 -
    1.98 -lemma le_cases_raw:
    1.99 -  shows "le_int_raw i j \<or> le_int_raw j i"
   1.100 -  by (cases i, cases j)
   1.101 -     (simp add: linorder_linear)
   1.102 -
   1.103  instance int :: linorder
   1.104  proof
   1.105    fix i j k :: int
   1.106    show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
   1.107 -    by (lifting le_antisym_raw)
   1.108 +    by (descending) (auto)
   1.109    show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
   1.110      by (auto simp add: less_int_def dest: antisym)
   1.111    show "i \<le> i"
   1.112 -    by (lifting le_refl_raw)
   1.113 +    by (descending) (auto)
   1.114    show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   1.115 -    by (lifting le_trans_raw)
   1.116 +    by (descending) (auto)
   1.117    show "i \<le> j \<or> j \<le> i"
   1.118 -    by (lifting le_cases_raw)
   1.119 +    by (descending) (auto)
   1.120  qed
   1.121  
   1.122  instantiation int :: distrib_lattice
   1.123 @@ -258,15 +204,11 @@
   1.124  
   1.125  end
   1.126  
   1.127 -lemma le_plus_int_raw:
   1.128 -  shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
   1.129 -  by (cases i, cases j, cases k) (simp)
   1.130 -
   1.131  instance int :: ordered_cancel_ab_semigroup_add
   1.132  proof
   1.133    fix i j k :: int
   1.134    show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   1.135 -    by (lifting le_plus_int_raw)
   1.136 +    by (descending) (auto)
   1.137  qed
   1.138  
   1.139  abbreviation
   1.140 @@ -296,7 +238,7 @@
   1.141    fixes k::int
   1.142    shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
   1.143    unfolding less_int_def int_of_nat
   1.144 -  by (lifting zero_le_imp_eq_int_raw)
   1.145 +  by (descending) (rule zero_le_imp_eq_int_raw)
   1.146  
   1.147  lemma zmult_zless_mono2:
   1.148    fixes i j k::int
   1.149 @@ -365,16 +307,10 @@
   1.150    shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
   1.151    by (auto iff: int_to_nat_raw_def)
   1.152  
   1.153 -lemma nat_le_eq_zle_raw:
   1.154 -  assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
   1.155 -  shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
   1.156 -  using a
   1.157 -  by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
   1.158 -
   1.159  lemma nat_le_eq_zle:
   1.160    fixes w z::"int"
   1.161    shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
   1.162    unfolding less_int_def
   1.163 -  by (lifting nat_le_eq_zle_raw)
   1.164 +  by (descending) (auto simp add: int_to_nat_raw_def)
   1.165  
   1.166  end
     2.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 01:38:29 2010 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Jun 29 02:18:08 2010 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4  text{*Proving that it is an equivalence relation*}
     2.5  
     2.6  lemma msgrel_refl: "X \<sim> X"
     2.7 -by (induct X, (blast intro: msgrel.intros)+)
     2.8 +by (induct X) (auto intro: msgrel.intros)
     2.9  
    2.10  theorem equiv_msgrel: "equivp msgrel"
    2.11  proof (rule equivpI)
    2.12 @@ -263,68 +263,47 @@
    2.13  
    2.14  subsection{*Injectivity Properties of Some Constructors*}
    2.15  
    2.16 -lemma NONCE_imp_eq:
    2.17 -  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
    2.18 -  by (drule msgrel_imp_eq_freenonces, simp)
    2.19 -
    2.20  text{*Can also be proved using the function @{term nonces}*}
    2.21  lemma Nonce_Nonce_eq [iff]:
    2.22    shows "(Nonce m = Nonce n) = (m = n)"
    2.23  proof
    2.24    assume "Nonce m = Nonce n"
    2.25 -  then show "m = n" by (lifting NONCE_imp_eq)
    2.26 +  then show "m = n" 
    2.27 +    by (descending) (drule msgrel_imp_eq_freenonces, simp)
    2.28  next
    2.29    assume "m = n"
    2.30    then show "Nonce m = Nonce n" by simp
    2.31  qed
    2.32  
    2.33 -lemma MPAIR_imp_eqv_left:
    2.34 -  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
    2.35 -  by (drule msgrel_imp_eqv_freeleft) (simp)
    2.36 -
    2.37  lemma MPair_imp_eq_left:
    2.38    assumes eq: "MPair X Y = MPair X' Y'"
    2.39    shows "X = X'"
    2.40 -  using eq by (lifting MPAIR_imp_eqv_left)
    2.41 -
    2.42 -lemma MPAIR_imp_eqv_right:
    2.43 -  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
    2.44 -  by (drule msgrel_imp_eqv_freeright) (simp)
    2.45 +  using eq 
    2.46 +  by (descending) (drule msgrel_imp_eqv_freeleft, simp)
    2.47  
    2.48  lemma MPair_imp_eq_right:
    2.49    shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
    2.50 -  by (lifting  MPAIR_imp_eqv_right)
    2.51 +  by (descending) (drule msgrel_imp_eqv_freeright, simp)
    2.52  
    2.53  theorem MPair_MPair_eq [iff]:
    2.54    shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
    2.55    by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
    2.56  
    2.57 -lemma NONCE_neqv_MPAIR:
    2.58 -  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
    2.59 -  by (auto dest: msgrel_imp_eq_freediscrim)
    2.60 -
    2.61  theorem Nonce_neq_MPair [iff]:
    2.62    shows "Nonce N \<noteq> MPair X Y"
    2.63 -  by (lifting NONCE_neqv_MPAIR)
    2.64 +  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
    2.65  
    2.66  text{*Example suggested by a referee*}
    2.67  
    2.68 -lemma CRYPT_NONCE_neq_NONCE:
    2.69 -  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
    2.70 -  by (auto dest: msgrel_imp_eq_freediscrim)
    2.71 -
    2.72  theorem Crypt_Nonce_neq_Nonce:
    2.73    shows "Crypt K (Nonce M) \<noteq> Nonce N"
    2.74 -  by (lifting CRYPT_NONCE_neq_NONCE)
    2.75 +  by (descending) (auto dest: msgrel_imp_eq_freediscrim) 
    2.76  
    2.77  text{*...and many similar results*}
    2.78 -lemma CRYPT2_NONCE_neq_NONCE:
    2.79 -  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
    2.80 -  by (auto dest: msgrel_imp_eq_freediscrim)
    2.81  
    2.82  theorem Crypt2_Nonce_neq_Nonce:
    2.83    shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
    2.84 -  by (lifting CRYPT2_NONCE_neq_NONCE)
    2.85 +  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
    2.86  
    2.87  theorem Crypt_Crypt_eq [iff]:
    2.88    shows "(Crypt K X = Crypt K X') = (X=X')"