# HG changeset patch # User Christian Urban # 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 \ 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 \ plus_int_raw j i" - by (cases i, cases j) (simp) - -lemma plus_zero_raw: - shows "plus_int_raw (0, 0) i \ i" - by (cases i) (simp) - -lemma plus_minus_zero_raw: - shows "plus_int_raw (uminus_int_raw i) i \ (0, 0)" - by (cases i) (simp) - -lemma times_assoc_raw: - shows "times_int_raw (times_int_raw i j) k \ 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 \ 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 \ i" - by (cases i) (simp) - -lemma times_plus_comm_raw: - shows "times_int_raw (plus_int_raw i j) k \ 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 "\ (0, 0) \ ((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 \ (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 \ le_int_raw j i \ i \ 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 \ le_int_raw j k \ le_int_raw i k" - by (cases i, cases j, cases k) (simp) - -lemma le_cases_raw: - shows "le_int_raw i j \ 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 \ j \ j \ i \ i = j" - by (lifting le_antisym_raw) + by (descending) (auto) show "(i < j) = (i \ j \ \ j \ i)" by (auto simp add: less_int_def dest: antisym) show "i \ i" - by (lifting le_refl_raw) + by (descending) (auto) show "i \ j \ j \ k \ i \ k" - by (lifting le_trans_raw) + by (descending) (auto) show "i \ j \ j \ 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 \ 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 \ j \ k + i \ k + j" - by (lifting le_plus_int_raw) + by (descending) (auto) qed abbreviation @@ -296,7 +238,7 @@ fixes k::int shows "0 < k \ \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 \ le_int_raw (0, 0) z" - shows "(int_to_nat_raw w \ 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 \ 0 \ z \ (int_to_nat w \ int_to_nat z) = (w \ 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 \ 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 \ NONCE n \ 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 \ MPAIR X' Y' \ X \ 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 \ MPAIR X' Y' \ Y \ 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' \ 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 "\(NONCE m \ MPAIR X Y)" - by (auto dest: msgrel_imp_eq_freediscrim) - theorem Nonce_neq_MPair [iff]: shows "Nonce N \ 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 "\(CRYPT K (NONCE M) \ NONCE N)" - by (auto dest: msgrel_imp_eq_freediscrim) - theorem Crypt_Nonce_neq_Nonce: shows "Crypt K (Nonce M) \ 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 "\(CRYPT K (CRYPT K' (NONCE M)) \ NONCE N)" - by (auto dest: msgrel_imp_eq_freediscrim) theorem Crypt2_Nonce_neq_Nonce: shows "Crypt K (Crypt K' (Nonce M)) \ 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')"