--- a/doc-src/IsarOverview/Isar/document/intro.tex Mon Dec 12 20:28:19 2011 +0100
+++ b/doc-src/IsarOverview/Isar/document/intro.tex Mon Dec 12 20:28:34 2011 +0100
@@ -116,7 +116,7 @@
is possible because Isar allows \isa{apply}-style proofs as components
of structured ones.
-Finally, do not be mislead by the simplicity of the formulae being proved,
+Finally, do not be misled by the simplicity of the formulae being proved,
especially in the beginning. Isar has been used very successfully in
large applications, for example the formalisation of Java
dialects~\cite{KleinN-TOPLAS}.
--- a/doc-src/IsarRef/Thy/Synopsis.thy Mon Dec 12 20:28:19 2011 +0100
+++ b/doc-src/IsarRef/Thy/Synopsis.thy Mon Dec 12 20:28:34 2011 +0100
@@ -302,7 +302,7 @@
have "a < b" sorry
also
- have "b\<le> c" sorry
+ have "b \<le> c" sorry
also
have "c = d" sorry
finally
@@ -318,7 +318,7 @@
\item The notion of @{text trans} rule is very general due to the
flexibility of Isabelle/Pure rule composition.
- \item User applications may declare there own rules, with some care
+ \item User applications may declare their own rules, with some care
about the operational details of higher-order unification.
\end{itemize}
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex Mon Dec 12 20:28:19 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Mon Dec 12 20:28:34 2011 +0100
@@ -691,7 +691,7 @@
\ \ \isacommand{also}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
\isanewline
\ \ \isacommand{also}\isamarkupfalse%
\isanewline
@@ -722,7 +722,7 @@
\item The notion of \isa{trans} rule is very general due to the
flexibility of Isabelle/Pure rule composition.
- \item User applications may declare there own rules, with some care
+ \item User applications may declare their own rules, with some care
about the operational details of higher-order unification.
\end{itemize}%
--- a/src/HOL/Quickcheck_Exhaustive.thy Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Mon Dec 12 20:28:34 2011 +0100
@@ -430,8 +430,8 @@
class fast_exhaustive = term_of +
fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
-consts throw_Counterexample :: "term list => unit"
-consts catch_Counterexample :: "unit => term list option"
+axiomatization throw_Counterexample :: "term list => unit"
+axiomatization catch_Counterexample :: "unit => term list option"
code_const throw_Counterexample
(Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
@@ -535,7 +535,16 @@
hide_fact orelse_def
no_notation orelse (infixr "orelse" 55)
-hide_const (open) orelse unknown mk_map_term check_all_n_lists
+
+hide_fact
+ exhaustive'_def
+ exhaustive_code_numeral'_def
+
+hide_const (open)
+ exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
+ throw_Counterexample catch_Counterexample
+ check_all enum_term_of
+ orelse unknown mk_map_term check_all_n_lists
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
--- a/src/HOL/Quickcheck_Narrowing.thy Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Mon Dec 12 20:28:34 2011 +0100
@@ -448,7 +448,7 @@
*)
hide_type code_int narrowing_type narrowing_term cons property
-hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists
+hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero
hide_const (open) Var Ctr "apply" sum cons
hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Mon Dec 12 20:28:34 2011 +0100
@@ -0,0 +1,287 @@
+(* Title: HOL/Quotient_Examples/Quotient_Rat.thy
+ Author: Cezary Kaliszyk
+
+Rational numbers defined with the quotient package, based on 'HOL/Rat.thy' by Makarius.
+*)
+
+theory Quotient_Rat imports Archimedean_Field
+ "~~/src/HOL/Library/Quotient_Product"
+begin
+
+definition
+ ratrel :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+ [simp]: "x \<approx> y \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
+
+lemma ratrel_equivp:
+ "part_equivp ratrel"
+proof (auto intro!: part_equivpI reflpI sympI transpI exI[of _ "1 :: int"])
+ fix a b c d e f :: int
+ assume nz: "d \<noteq> 0" "b \<noteq> 0"
+ assume y: "a * d = c * b"
+ assume x: "c * f = e * d"
+ then have "c * b * f = e * d * b" using nz by simp
+ then have "a * d * f = e * d * b" using y by simp
+ then show "a * f = e * b" using nz by simp
+qed
+
+quotient_type rat = "int \<times> int" / partial: ratrel
+ using ratrel_equivp .
+
+instantiation rat :: "{zero, one, plus, uminus, minus, times, ord, abs_if, sgn_if}"
+begin
+
+quotient_definition
+ "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)"
+
+quotient_definition
+ "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)"
+
+fun times_rat_raw where
+ "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
+
+quotient_definition
+ "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw
+
+fun plus_rat_raw where
+ "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
+
+quotient_definition
+ "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw
+
+fun uminus_rat_raw where
+ "uminus_rat_raw (a :: int, b :: int) = (-a, b)"
+
+quotient_definition
+ "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw"
+
+definition
+ minus_rat_def: "a - b = a + (-b\<Colon>rat)"
+
+fun le_rat_raw where
+ "le_rat_raw (a :: int, b) (c, d) \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)"
+
+quotient_definition
+ "(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw"
+
+definition
+ less_rat_def: "(z\<Colon>rat) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+ rabs_rat_def: "\<bar>i\<Colon>rat\<bar> = (if i < 0 then - i else i)"
+
+definition
+ sgn_rat_def: "sgn (i\<Colon>rat) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
+
+instance by intro_classes
+ (auto simp add: rabs_rat_def sgn_rat_def)
+
+end
+
+definition
+ Fract_raw :: "int \<Rightarrow> int \<Rightarrow> (int \<times> int)"
+where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))"
+
+quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is
+ Fract_raw
+
+lemma [quot_respect]:
+ "(op \<approx> ===> op \<approx> ===> op \<approx>) times_rat_raw times_rat_raw"
+ "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_rat_raw plus_rat_raw"
+ "(op \<approx> ===> op \<approx>) uminus_rat_raw uminus_rat_raw"
+ "(op = ===> op = ===> op \<approx>) Fract_raw Fract_raw"
+ by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2))
+
+lemmas [simp] = Respects_def
+
+instantiation rat :: comm_ring_1
+begin
+
+instance proof
+ fix a b c :: rat
+ show "a * b * c = a * (b * c)"
+ by partiality_descending auto
+ show "a * b = b * a"
+ by partiality_descending auto
+ show "1 * a = a"
+ by partiality_descending auto
+ show "a + b + c = a + (b + c)"
+ by partiality_descending (auto simp add: mult_commute right_distrib)
+ show "a + b = b + a"
+ by partiality_descending auto
+ show "0 + a = a"
+ by partiality_descending auto
+ show "- a + a = 0"
+ by partiality_descending auto
+ show "a - b = a + - b"
+ by (simp add: minus_rat_def)
+ show "(a + b) * c = a * c + b * c"
+ by partiality_descending (auto simp add: mult_commute right_distrib)
+ show "(0 :: rat) \<noteq> (1 :: rat)"
+ by partiality_descending auto
+qed
+
+end
+
+lemma add_one_Fract: "1 + Fract (int k) 1 = Fract (1 + int k) 1"
+ by descending auto
+
+lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
+ apply (induct k)
+ apply (simp add: zero_rat_def Fract_def)
+ apply (simp add: add_one_Fract)
+ done
+
+lemma of_int_rat: "of_int k = Fract k 1"
+ apply (cases k rule: int_diff_cases)
+ apply (auto simp add: of_nat_rat minus_rat_def)
+ apply descending
+ apply auto
+ done
+
+instantiation rat :: number_ring
+begin
+
+definition
+ rat_number_of_def: "number_of w = Fract w 1"
+
+instance apply default
+ unfolding rat_number_of_def of_int_rat ..
+
+end
+
+instantiation rat :: field_inverse_zero begin
+
+fun rat_inverse_raw where
+ "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
+
+quotient_definition
+ "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw
+
+definition
+ divide_rat_def: "q / r = q * inverse (r::rat)"
+
+lemma [quot_respect]:
+ "(op \<approx> ===> op \<approx>) rat_inverse_raw rat_inverse_raw"
+ by (auto intro!: fun_relI simp add: mult_commute)
+
+instance proof
+ fix q :: rat
+ assume "q \<noteq> 0"
+ then show "inverse q * q = 1"
+ by partiality_descending auto
+next
+ fix q r :: rat
+ show "q / r = q * inverse r" by (simp add: divide_rat_def)
+next
+ show "inverse 0 = (0::rat)" by partiality_descending auto
+qed
+
+end
+
+lemma [quot_respect]: "(op \<approx> ===> op \<approx> ===> op =) le_rat_raw le_rat_raw"
+proof -
+ {
+ fix a b c d e f g h :: int
+ assume "a * f * (b * f) \<le> e * b * (b * f)"
+ then have le: "a * f * b * f \<le> e * b * b * f" by simp
+ assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
+ then have b2: "b * b > 0"
+ by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+ have f2: "f * f > 0" using nz(3)
+ by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+ assume eq: "a * d = c * b" "e * h = g * f"
+ have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
+ by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+ then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
+ by (metis (no_types) mult_assoc mult_commute)
+ then have "c * f * f * d \<le> e * f * d * d" using b2
+ by (metis leD linorder_le_less_linear mult_strict_right_mono)
+ then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
+ by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+ then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
+ by (metis (no_types) mult_assoc mult_commute)
+ then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
+ by (metis leD linorder_le_less_linear mult_strict_right_mono)
+ }
+ then show ?thesis by (auto intro!: fun_relI)
+qed
+
+instantiation rat :: linorder
+begin
+
+instance proof
+ fix q r s :: rat
+ {
+ assume "q \<le> r" and "r \<le> s"
+ then show "q \<le> s"
+ proof (partiality_descending, auto simp add: mult_assoc[symmetric])
+ fix a b c d e f :: int
+ assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0"
+ then have d2: "d * d > 0"
+ by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+ assume le: "a * d * b * d \<le> c * b * b * d" "c * f * d * f \<le> e * d * d * f"
+ then have a: "a * d * b * d * f * f \<le> c * b * b * d * f * f" using nz(3)
+ by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+ have "c * f * d * f * b * b \<le> e * d * d * f * b * b" using nz(1) le
+ by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+ then have "a * f * b * f * (d * d) \<le> e * b * b * f * (d * d)" using a
+ by (simp add: algebra_simps)
+ then show "a * f * b * f \<le> e * b * b * f" using d2
+ by (metis leD linorder_le_less_linear mult_strict_right_mono)
+ qed
+ next
+ assume "q \<le> r" and "r \<le> q"
+ then show "q = r"
+ apply (partiality_descending, auto)
+ apply (case_tac "b > 0", case_tac [!] "ba > 0")
+ apply simp_all
+ done
+ next
+ show "q \<le> q" by partiality_descending auto
+ show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
+ unfolding less_rat_def
+ by partiality_descending (auto simp add: le_less mult_commute)
+ show "q \<le> r \<or> r \<le> q"
+ by partiality_descending (auto simp add: mult_commute linorder_linear)
+ }
+qed
+
+end
+
+instance rat :: archimedean_field
+proof
+ fix q r s :: rat
+ show "q \<le> r ==> s + q \<le> s + r"
+ proof (partiality_descending, auto simp add: algebra_simps, simp add: mult_assoc[symmetric])
+ fix a b c d e :: int
+ assume "e \<noteq> 0"
+ then have e2: "e * e > 0"
+ by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+ assume "a * b * d * d \<le> b * b * c * d"
+ then show "a * b * d * d * e * e * e * e \<le> b * b * c * d * e * e * e * e"
+ using e2 by (metis comm_mult_left_mono mult_commute linorder_le_cases
+ mult_left_mono_neg)
+ qed
+ show "q < r ==> 0 < s ==> s * q < s * r" unfolding less_rat_def
+ proof (partiality_descending, auto simp add: algebra_simps, simp add: mult_assoc[symmetric])
+ fix a b c d e f :: int
+ assume a: "e \<noteq> 0" "f \<noteq> 0" "0 \<le> e * f" "a * b * d * d \<le> b * b * c * d"
+ have "a * b * d * d * (e * f) \<le> b * b * c * d * (e * f)" using a
+ by (simp add: mult_right_mono)
+ then show "a * b * d * d * e * f * f * f \<le> b * b * c * d * e * f * f * f"
+ by (simp add: mult_assoc[symmetric]) (metis a(3) comm_mult_left_mono
+ mult_commute mult_left_mono_neg zero_le_mult_iff)
+ qed
+ show "\<exists>z. r \<le> of_int z"
+ unfolding of_int_rat
+ proof (partiality_descending, auto)
+ fix a b :: int
+ assume "b \<noteq> 0"
+ then have "a * b \<le> (a div b + 1) * b * b"
+ by (metis mult_commute div_mult_self1_is_id less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
+ then show "\<exists>z\<Colon>int. a * b \<le> z * b * b" by auto
+ qed
+qed
+
+end
--- a/src/HOL/Quotient_Examples/ROOT.ML Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/Quotient_Examples/ROOT.ML Mon Dec 12 20:28:34 2011 +0100
@@ -5,5 +5,5 @@
*)
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
- "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun"];
+ "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];
--- a/src/HOL/Rat.thy Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/Rat.thy Mon Dec 12 20:28:34 2011 +0100
@@ -1158,7 +1158,7 @@
begin
definition
- "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
+ "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive (%l. Quickcheck_Exhaustive.exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
instance ..
@@ -1168,7 +1168,7 @@
begin
definition
- "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
+ "full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k.
f (let j = Code_Numeral.int_of l + 1
in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
--- a/src/HOL/RealDef.thy Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/RealDef.thy Mon Dec 12 20:28:34 2011 +0100
@@ -1729,7 +1729,7 @@
begin
definition
- "exhaustive f d = exhaustive (%r. f (Ratreal r)) d"
+ "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"
instance ..
@@ -1739,7 +1739,7 @@
begin
definition
- "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d"
+ "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"
instance ..
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 12 20:28:34 2011 +0100
@@ -113,7 +113,7 @@
!current_result)
| SOME test_fun =>
let
- val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "...");
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
val (response, exec_time) =
cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
val _ = Quickcheck.add_response names eval_terms response current_result
--- a/src/HOL/Word/Word.thy Mon Dec 12 20:28:19 2011 +0100
+++ b/src/HOL/Word/Word.thy Mon Dec 12 20:28:34 2011 +0100
@@ -140,7 +140,7 @@
lemma
uint_0:"0 <= uint x" and
uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
- by (auto simp: uint [simplified])
+ by (auto simp: uint [unfolded atLeastLessThan_iff])
lemma uint_mod_same:
"uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
@@ -169,7 +169,7 @@
lemmas td_uint = word_uint.td_thm
lemmas td_ext_ubin = td_ext_uint
- [simplified len_gt_0 no_bintr_alt1 [symmetric]]
+ [unfolded len_gt_0 no_bintr_alt1 [symmetric]]
interpretation word_ubin:
td_ext "uint::'a::len0 word \<Rightarrow> int"
@@ -744,14 +744,14 @@
"{bl. length bl = len_of TYPE('a::len0)}"
by (rule td_bl)
-lemmas word_bl_Rep' = word_bl.Rep [simplified, iff]
+lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
lemma word_size_bl: "size w = size (to_bl w)"
unfolding word_size by auto
lemma to_bl_use_of_bl:
"(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
- by (fastforce elim!: word_bl.Abs_inverse [simplified])
+ by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
@@ -1153,7 +1153,7 @@
apply simp
done
-lemmas size_0_same = size_0_same' [folded word_size]
+lemmas size_0_same = size_0_same' [unfolded word_size]
lemmas unat_eq_0 = unat_0_iff
lemmas unat_eq_zero = unat_0_iff
@@ -1222,7 +1222,8 @@
simp add: pred_def succ_def add_commute mult_commute
ring_distribs new_word_of_int_homs)+
-lemmas uint_cong = arg_cong [where f = uint]
+lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
+ by simp
lemmas uint_word_ariths =
word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
@@ -1268,11 +1269,13 @@
"0 <= (y :: 'a :: len0 word)"
unfolding word_le_def by auto
-lemma word_m1_ge [simp] : "word_pred 0 >= y"
+lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
unfolding word_le_def
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
-lemmas word_n1_ge [simp] = word_m1_ge [simplified word_sp_01]
+lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"
+ unfolding word_le_def
+ by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
lemmas word_not_simps [simp] =
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
@@ -1610,9 +1613,9 @@
apply (rule uint_sub_ge)
done
-lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, simplified]
-lemmas udvd_incr0 = udvd_incr' [where ua=0, simplified]
-lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
+lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
+lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
+lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
lemma udvd_minus_le':
"xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
@@ -1830,13 +1833,14 @@
Abs_fnat_hom_1 word_arith_nat_div
word_arith_nat_mod
-lemmas unat_cong = arg_cong [where f = unat]
+lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
+ by simp
lemmas unat_word_ariths = word_arith_nat_defs
[THEN trans [OF unat_cong unat_of_nat]]
lemmas word_sub_less_iff = word_sub_le_iff
- [simplified linorder_not_less [symmetric], simplified]
+ [unfolded linorder_not_less [symmetric] Not_eq_iff]
lemma unat_add_lem:
"(unat x + unat y < 2 ^ len_of TYPE('a)) =
@@ -2808,11 +2812,14 @@
apply (auto simp add : shiftl1_rev)
done
-lemmas rev_shiftl =
- shiftl_rev [where w = "word_reverse w", simplified] for w
-
-lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal']
-lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal']
+lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
+ by (simp add: shiftl_rev)
+
+lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
+ by (simp add: rev_shiftl)
+
+lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
+ by (simp add: shiftr_rev)
lemma bl_sshiftr1:
"to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
@@ -3357,14 +3364,13 @@
lemma ucast_slice: "ucast w = slice 0 w"
unfolding slice_def by (simp add : ucast_slice1)
-lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
-
-lemma revcast_slice1':
+lemma slice_id: "slice 0 t = t"
+ by (simp only: ucast_slice [symmetric] ucast_id)
+
+lemma revcast_slice1 [OF refl]:
"rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
unfolding slice1_def revcast_def' by (simp add : word_size)
-lemmas revcast_slice1 = refl [THEN revcast_slice1']
-
lemma slice1_tf_tf':
"to_bl (slice1 n w :: 'a :: len0 word) =
rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
@@ -3385,17 +3391,14 @@
apply (simp add: word_bl.Abs_inverse)
done
-lemma rev_slice':
- "res = slice n (word_reverse w) \<Longrightarrow> n + k + size res = size w \<Longrightarrow>
- res = word_reverse (slice k w)"
+lemma rev_slice:
+ "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
+ slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
apply (unfold slice_def word_size)
- apply clarify
apply (rule rev_slice1)
apply arith
done
-lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
-
lemmas sym_notr =
not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
@@ -3607,14 +3610,13 @@
apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
done
-lemma slice_cat1':
+lemma slice_cat1 [OF refl]:
"wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
apply safe
apply (rule word_eqI)
apply (simp add: nth_slice test_bit_cat word_size)
done
-lemmas slice_cat1 = refl [THEN slice_cat1']
lemmas slice_cat2 = trans [OF slice_id word_cat_id]
lemma cat_slices:
@@ -3688,11 +3690,10 @@
lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
-lemma nth_rcat_lem' [rule_format] :
- "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> (ALL n. n < size wl * sw -->
- rev (concat (map to_bl wl)) ! n =
- rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
- apply (unfold word_size)
+lemma nth_rcat_lem:
+ "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
+ rev (concat (map to_bl wl)) ! n =
+ rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
apply (induct "wl")
apply clarsimp
apply (clarsimp simp add : nth_append size_rcat_lem)
@@ -3701,8 +3702,6 @@
apply clarsimp
done
-lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
-
lemma test_bit_rcat:
"sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
(n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
@@ -3714,9 +3713,9 @@
test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
done
-lemma foldl_eq_foldr [rule_format] :
- "ALL x. foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
- by (induct xs) (auto simp add : add_assoc)
+lemma foldl_eq_foldr:
+ "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
+ by (induct xs arbitrary: x) (auto simp add : add_assoc)
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
@@ -3725,15 +3724,13 @@
test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
-- "lazy way of expressing that u and v, and su and sv, have same types"
-lemma word_rsplit_len_indep':
+lemma word_rsplit_len_indep [OF refl refl refl refl]:
"[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
word_rsplit v = sv \<Longrightarrow> length su = length sv"
apply (unfold word_rsplit_def)
apply (auto simp add : bin_rsplit_len_indep)
done
-lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
-
lemma length_word_rsplit_size:
"n = len_of TYPE ('a :: len) \<Longrightarrow>
(length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
@@ -3744,7 +3741,7 @@
lemmas length_word_rsplit_lt_size =
length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
-lemma length_word_rsplit_exp_size:
+lemma length_word_rsplit_exp_size:
"n = len_of TYPE ('a :: len) \<Longrightarrow>
length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
@@ -3770,24 +3767,21 @@
apply (erule xtr7, rule len_gt_0 [THEN dtle])+
done
-lemma size_word_rsplit_rcat_size':
- "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>
- size frcw = length ws * len_of TYPE ('a) \<Longrightarrow>
- size (hd [word_rsplit frcw, ws]) = size ws"
+lemma size_word_rsplit_rcat_size:
+ "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
+ size frcw = length ws * len_of TYPE('a)\<rbrakk>
+ \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
apply (fast intro: given_quot_alt)
done
-lemmas size_word_rsplit_rcat_size =
- size_word_rsplit_rcat_size' [simplified]
-
lemma msrevs:
fixes n::nat
shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
and "(k * n + m) mod n = m mod n"
by (auto simp: add_commute)
-lemma word_rsplit_rcat_size':
+lemma word_rsplit_rcat_size [OF refl]:
"word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>
size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws"
apply (frule size_word_rsplit_rcat_size, assumption)
@@ -3811,8 +3805,6 @@
apply simp_all
done
-lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
-
subsection "Rotation"
@@ -3860,7 +3852,8 @@
lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
-lemmas rotater_rev = rotater_rev' [where xs = "rev ys", simplified] for ys
+lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
+ using rotater_rev' [where xs = "rev ys"] by simp
lemma rotater_drop_take:
"rotater n xs =