author Christian Urban Tue Jun 29 02:18:08 2010 +0100 (2010-06-29) changeset 37594 32ad67684ee7 parent 37593 2505feaf2d70 child 37608 165cd386288d
cosmetics: avoided statement of raw theorems, used the method descending instead
```     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.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.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.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.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.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.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')"
```