--- a/src/HOL/Word/BinBoolList.thy Thu Nov 08 20:08:00 2007 +0100
+++ b/src/HOL/Word/BinBoolList.thy Thu Nov 08 20:08:01 2007 +0100
@@ -281,7 +281,7 @@
apply arith
done
-lemmas nth_rev_alt = nth_rev [where xs = "rev ?ys", simplified]
+lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified, standard]
lemma nth_bin_to_bl_aux [rule_format] :
"ALL w n bl. n < m + length bl --> (bin_to_bl_aux m w bl) ! n =
@@ -346,7 +346,7 @@
done
lemmas butlast_bin_rest = butlast_rest_bin
- [where w="bl_to_bin ?bl" and n="length ?bl", simplified]
+ [where w="bl_to_bin bl" and n="length bl", simplified, standard]
lemma butlast_rest_bl2bin_aux [rule_format] :
"ALL w. bl ~= [] -->
@@ -924,7 +924,7 @@
lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
-lemmas seqr = eq_reflection [where x = "size ?w"]
+lemmas seqr = eq_reflection [where x = "size w", standard]
lemmas tl_Nil = tl.simps (1)
lemmas tl_Cons = tl.simps (2)
@@ -963,9 +963,9 @@
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
lemmas rsplit_aux_simps = bin_rsplit_aux_simps
-lemmas th_if_simp1 = split_if [where P = "op = ?l",
+lemmas th_if_simp1 = split_if [where P = "op = l",
THEN iffD1, THEN conjunct1, THEN mp, standard]
-lemmas th_if_simp2 = split_if [where P = "op = ?l",
+lemmas th_if_simp2 = split_if [where P = "op = l",
THEN iffD1, THEN conjunct2, THEN mp, standard]
lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
--- a/src/HOL/Word/WordArith.thy Thu Nov 08 20:08:00 2007 +0100
+++ b/src/HOL/Word/WordArith.thy Thu Nov 08 20:08:01 2007 +0100
@@ -34,22 +34,22 @@
by (auto simp: udvd_def)
lemmas word_div_no [simp] =
- word_div_def [of "number_of ?a" "number_of ?b"]
+ word_div_def [of "number_of a" "number_of b", standard]
lemmas word_mod_no [simp] =
- word_mod_def [of "number_of ?a" "number_of ?b"]
+ word_mod_def [of "number_of a" "number_of b", standard]
lemmas word_less_no [simp] =
- word_less_def [of "number_of ?a" "number_of ?b"]
+ word_less_def [of "number_of a" "number_of b", standard]
lemmas word_le_no [simp] =
- word_le_def [of "number_of ?a" "number_of ?b"]
+ word_le_def [of "number_of a" "number_of b", standard]
lemmas word_sless_no [simp] =
- word_sless_def [of "number_of ?a" "number_of ?b"]
+ word_sless_def [of "number_of a" "number_of b", standard]
lemmas word_sle_no [simp] =
- word_sle_def [of "number_of ?a" "number_of ?b"]
+ word_sle_def [of "number_of a" "number_of b", standard]
(* following two are available in class number_ring,
but convenient to have them here here;
@@ -351,7 +351,7 @@
lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))"
unfolding word_less_def by auto
-lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of ?y"]
+lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y", standard]
lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
unfolding word_sle_def word_sless_def
@@ -1165,10 +1165,10 @@
lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
word_le_minus_cancel word_le_minus_mono_left
-lemmas word_l_diffs = mcs [where y = "?w + ?x", unfolded add_diff_cancel]
-lemmas word_diff_ls = mcs [where z = "?w + ?x", unfolded add_diff_cancel]
+lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel, standard]
+lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel, standard]
lemmas word_plus_mcs = word_diff_ls
- [where y = "?v + ?x", unfolded add_diff_cancel]
+ [where y = "v + x", unfolded add_diff_cancel, standard]
lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
--- a/src/HOL/Word/WordBitwise.thy Thu Nov 08 20:08:00 2007 +0100
+++ b/src/HOL/Word/WordBitwise.thy Thu Nov 08 20:08:01 2007 +0100
@@ -22,10 +22,10 @@
word_and_def word_or_def word_xor_def
lemmas word_no_log_defs [simp] =
- word_not_def [where a="number_of ?a",
- unfolded word_no_wi wils1, folded word_no_wi]
- word_log_binary_defs [where a="number_of ?a" and b="number_of ?b",
- unfolded word_no_wi wils1, folded word_no_wi]
+ word_not_def [where a="number_of a",
+ unfolded word_no_wi wils1, folded word_no_wi, standard]
+ word_log_binary_defs [where a="number_of a" and b="number_of b",
+ unfolded word_no_wi wils1, folded word_no_wi, standard]
lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
--- a/src/HOL/Word/WordShift.thy Thu Nov 08 20:08:00 2007 +0100
+++ b/src/HOL/Word/WordShift.thy Thu Nov 08 20:08:01 2007 +0100
@@ -171,7 +171,7 @@
subsubsection "shift functions in terms of lists of bools"
lemmas bshiftr1_no_bin [simp] =
- bshiftr1_def [where w="number_of ?w", unfolded to_bl_no_bin]
+ bshiftr1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
@@ -180,8 +180,12 @@
unfolding uint_bl of_bl_no
by (simp add: bl_to_bin_aux_append bl_to_bin_def)
-lemmas shiftl1_bl = shiftl1_of_bl
- [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified]
+lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
+proof -
+ have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
+ also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
+ finally show ?thesis .
+qed
lemma bl_shiftl1:
"to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
@@ -220,7 +224,7 @@
done
lemmas rev_shiftl =
- shiftl_rev [where w = "word_reverse ?w1", simplified, standard]
+ shiftl_rev [where w = "word_reverse w", simplified, standard]
lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal', standard]
lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
@@ -301,10 +305,15 @@
unfolding shiftl_def
by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
-lemmas shiftl_bl =
- shiftl_of_bl [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified]
+lemma shiftl_bl:
+ "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
+proof -
+ have "w << n = of_bl (to_bl w) << n" by simp
+ also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
+ finally show ?thesis .
+qed
-lemmas shiftl_number [simp] = shiftl_def [where w="number_of ?w"]
+lemmas shiftl_number [simp] = shiftl_def [where w="number_of w", standard]
lemma bl_shiftl:
"to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
@@ -366,10 +375,10 @@
done
lemmas sshiftr_no [simp] =
- sshiftr_no' [where w = "number_of ?w", OF refl, unfolded word_size]
+ sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
lemmas shiftr_no [simp] =
- shiftr_no' [where w = "number_of ?w", OF refl, unfolded word_size]
+ shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
lemma shiftr1_bl_of':
"us = shiftr1 (of_bl bl) ==> length bl <= size us ==>
@@ -597,7 +606,7 @@
lemmas revcast_def' = revcast_def [simplified]
lemmas revcast_def'' = revcast_def' [simplified word_size]
lemmas revcast_no_def [simp] =
- revcast_def' [where w="number_of ?w", unfolded word_size]
+ revcast_def' [where w="number_of w", unfolded word_size, standard]
lemma to_bl_revcast:
"to_bl (revcast w :: 'a :: len0 word) =
@@ -618,7 +627,7 @@
lemmas revcast_rev_ucast = revcast_rev_ucast' [OF refl refl refl]
lemmas revcast_ucast = revcast_rev_ucast
- [where w = "word_reverse ?w1", simplified word_rev_rev, standard]
+ [where w = "word_reverse w", simplified word_rev_rev, standard]
lemmas ucast_revcast = revcast_rev_ucast [THEN word_rev_gal', standard]
lemmas ucast_rev_revcast = revcast_ucast [THEN word_rev_gal', standard]
@@ -718,7 +727,7 @@
subsubsection "Slices"
lemmas slice1_no_bin [simp] =
- slice1_def [where w="number_of ?w", unfolded to_bl_no_bin]
+ slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
lemmas slice_no_bin [simp] =
trans [OF slice_def [THEN meta_eq_to_obj_eq]
@@ -1066,12 +1075,12 @@
done
lemmas word_cat_bl_no_bin [simp] =
- word_cat_bl [where a="number_of ?a"
- and b="number_of ?b",
- unfolded to_bl_no_bin]
+ word_cat_bl [where a="number_of a"
+ and b="number_of b",
+ unfolded to_bl_no_bin, standard]
lemmas word_split_bl_no_bin [simp] =
- word_split_bl_eq [where c="number_of ?c", unfolded to_bl_no_bin]
+ word_split_bl_eq [where c="number_of c", unfolded to_bl_no_bin, standard]
-- {* this odd result arises from the fact that the statement of the
result implies that the decoded words are of the same type,
@@ -1288,7 +1297,7 @@
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]
+lemmas rotater_rev = rotater_rev' [where xs = "rev ys", simplified, standard]
lemma rotater_drop_take:
"rotater n xs =
@@ -1588,10 +1597,10 @@
unfolding word_roti_def by auto
lemmas word_rotr_dt_no_bin' [simp] =
- word_rotr_dt [where w="number_of ?w", unfolded to_bl_no_bin]
+ word_rotr_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
lemmas word_rotl_dt_no_bin' [simp] =
- word_rotl_dt [where w="number_of ?w", unfolded to_bl_no_bin]
+ word_rotl_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
declare word_roti_def [simp]