# HG changeset patch
# User wenzelm
# Date 1194548881 -3600
# Node ID a5fcf6d12a535d93129a430b3f7d7b417282d9fa
# Parent  0d46bea017418c1fc2fc6037a51f809f65507596
eliminated illegal schematic variables in where/of;

diff -r 0d46bea01741 -r a5fcf6d12a53 src/HOL/Word/BinBoolList.thy
--- 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]
diff -r 0d46bea01741 -r a5fcf6d12a53 src/HOL/Word/WordArith.thy
--- 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]
 
diff -r 0d46bea01741 -r a5fcf6d12a53 src/HOL/Word/WordBitwise.thy
--- 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]
 
diff -r 0d46bea01741 -r a5fcf6d12a53 src/HOL/Word/WordShift.thy
--- 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]