# HG changeset patch
# User wenzelm
# Date 1194548880 -3600
# Node ID 0d46bea017418c1fc2fc6037a51f809f65507596
# Parent  510b469878867eb1ca740f125676862d59b88261
eliminated illegal schematic variables in where/of;
tuned;

diff -r 510b46987886 -r 0d46bea01741 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Thu Nov 08 20:07:58 2007 +0100
+++ b/src/HOL/IntDef.thy	Thu Nov 08 20:08:00 2007 +0100
@@ -677,51 +677,51 @@
   by (cases z rule: int_cases) auto
 
 text{*Contributed by Brian Huffman*}
-theorem int_diff_cases [case_names diff]:
-assumes prem: "!!m n. (z\<Colon>int) = of_nat m - of_nat n ==> P" shows "P"
+theorem int_diff_cases:
+  obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
 apply (cases z rule: eq_Abs_Integ)
-apply (rule_tac m=x and n=y in prem)
+apply (rule_tac m=x and n=y in diff)
 apply (simp add: int_def diff_def minus add)
 done
 
 
 subsection {* Legacy theorems *}
 
-lemmas zminus_zminus = minus_minus [of "?z::int"]
+lemmas zminus_zminus = minus_minus [of "z::int", standard]
 lemmas zminus_0 = minus_zero [where 'a=int]
-lemmas zminus_zadd_distrib = minus_add_distrib [of "?z::int" "?w"]
-lemmas zadd_commute = add_commute [of "?z::int" "?w"]
-lemmas zadd_assoc = add_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
-lemmas zadd_left_commute = add_left_commute [of "?x::int" "?y" "?z"]
+lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
+lemmas zadd_commute = add_commute [of "z::int" "w", standard]
+lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
+lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
 lemmas zmult_ac = OrderedGroup.mult_ac
-lemmas zadd_0 = OrderedGroup.add_0_left [of "?z::int"]
-lemmas zadd_0_right = OrderedGroup.add_0_left [of "?z::int"]
-lemmas zadd_zminus_inverse2 = left_minus [of "?z::int"]
-lemmas zmult_zminus = mult_minus_left [of "?z::int" "?w"]
-lemmas zmult_commute = mult_commute [of "?z::int" "?w"]
-lemmas zmult_assoc = mult_assoc [of "?z1.0::int" "?z2.0" "?z3.0"]
-lemmas zadd_zmult_distrib = left_distrib [of "?z1.0::int" "?z2.0" "?w"]
-lemmas zadd_zmult_distrib2 = right_distrib [of "?w::int" "?z1.0" "?z2.0"]
-lemmas zdiff_zmult_distrib = left_diff_distrib [of "?z1.0::int" "?z2.0" "?w"]
-lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "?w::int" "?z1.0" "?z2.0"]
+lemmas zadd_0 = OrderedGroup.add_0_left [of "z::int", standard]
+lemmas zadd_0_right = OrderedGroup.add_0_left [of "z::int", standard]
+lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
+lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
+lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
+lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
+lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
+lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
+lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
+lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
 
 lemmas int_distrib =
   zadd_zmult_distrib zadd_zmult_distrib2
   zdiff_zmult_distrib zdiff_zmult_distrib2
 
-lemmas zmult_1 = mult_1_left [of "?z::int"]
-lemmas zmult_1_right = mult_1_right [of "?z::int"]
+lemmas zmult_1 = mult_1_left [of "z::int", standard]
+lemmas zmult_1_right = mult_1_right [of "z::int", standard]
 
-lemmas zle_refl = order_refl [of "?w::int"]
-lemmas zle_trans = order_trans [where 'a=int and x="?i" and y="?j" and z="?k"]
-lemmas zle_anti_sym = order_antisym [of "?z::int" "?w"]
-lemmas zle_linear = linorder_linear [of "?z::int" "?w"]
+lemmas zle_refl = order_refl [of "w::int", standard]
+lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
+lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
+lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
 lemmas zless_linear = linorder_less_linear [where 'a = int]
 
-lemmas zadd_left_mono = add_left_mono [of "?i::int" "?j" "?k"]
-lemmas zadd_strict_right_mono = add_strict_right_mono [of "?i::int" "?j" "?k"]
-lemmas zadd_zless_mono = add_less_le_mono [of "?w'::int" "?w" "?z'" "?z"]
+lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
+lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
+lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
 
 lemmas int_0_less_1 = zero_less_one [where 'a=int]
 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
@@ -731,17 +731,17 @@
 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
 lemmas int_mult = of_nat_mult [where 'a=int]
 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
-lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="?n"]
+lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
 lemmas zless_int = of_nat_less_iff [where 'a=int]
-lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="?k"]
+lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
-lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="?n"]
+lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
 lemmas int_0 = of_nat_0 [where 'a=int]
 lemmas int_1 = of_nat_1 [where 'a=int]
 lemmas int_Suc = of_nat_Suc [where 'a=int]
-lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"]
+lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
 lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
diff -r 510b46987886 -r 0d46bea01741 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Thu Nov 08 20:07:58 2007 +0100
+++ b/src/HOL/Word/BinGeneral.thy	Thu Nov 08 20:08:00 2007 +0100
@@ -304,42 +304,42 @@
   done
 
 lemmas bintrunc_Pls = 
-  bintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps]
+  bintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps, standard]
 
 lemmas bintrunc_Min [simp] = 
-  bintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps]
+  bintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps, standard]
 
 lemmas bintrunc_BIT  [simp] = 
-  bintrunc.Suc [where bin="?w BIT ?b", simplified bin_last_simps bin_rest_simps]
+  bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
 
 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
 
 lemmas sbintrunc_Suc_Pls = 
-  sbintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps]
+  sbintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps, standard]
 
 lemmas sbintrunc_Suc_Min = 
-  sbintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps]
+  sbintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps, standard]
 
 lemmas sbintrunc_Suc_BIT [simp] = 
-  sbintrunc.Suc [where bin="?w BIT ?b", simplified bin_last_simps bin_rest_simps]
+  sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
 
 lemmas sbintrunc_Pls = 
   sbintrunc.Z [where bin="Numeral.Pls", 
-               simplified bin_last_simps bin_rest_simps bit.simps]
+               simplified bin_last_simps bin_rest_simps bit.simps, standard]
 
 lemmas sbintrunc_Min = 
   sbintrunc.Z [where bin="Numeral.Min", 
-               simplified bin_last_simps bin_rest_simps bit.simps]
+               simplified bin_last_simps bin_rest_simps bit.simps, standard]
 
 lemmas sbintrunc_0_BIT_B0 [simp] = 
-  sbintrunc.Z [where bin="?w BIT bit.B0", 
-               simplified bin_last_simps bin_rest_simps bit.simps]
+  sbintrunc.Z [where bin="w BIT bit.B0", 
+               simplified bin_last_simps bin_rest_simps bit.simps, standard]
 
 lemmas sbintrunc_0_BIT_B1 [simp] = 
-  sbintrunc.Z [where bin="?w BIT bit.B1", 
-               simplified bin_last_simps bin_rest_simps bit.simps]
+  sbintrunc.Z [where bin="w BIT bit.B1", 
+               simplified bin_last_simps bin_rest_simps bit.simps, standard]
 
 lemmas sbintrunc_0_simps =
   sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
@@ -369,7 +369,7 @@
   "sbintrunc n Numeral.Min = Numeral.Min"
   by (induct n) auto
 
-lemmas thobini1 = arg_cong [where f = "%w. w BIT ?b"]
+lemmas thobini1 = arg_cong [where f = "%w. w BIT b", standard]
 
 lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
 lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
@@ -500,29 +500,35 @@
   apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
   done
 
-lemmas sb_inc_lem = int_mod_ge' 
-  [where n = "2 ^ (Suc ?k)" and b = "?a + 2 ^ ?k", 
-   simplified zless2p, OF _ TrueI]
+lemma sb_inc_lem:
+  "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+  apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
+  apply (rule TrueI)
+  done
 
-lemmas sb_inc_lem' = 
-  iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0]
+lemma sb_inc_lem':
+  "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+  by (rule iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0])
 
 lemma sbintrunc_inc:
-  "x < - (2 ^ n) ==> x + 2 ^ (Suc n) <= sbintrunc n x"
+  "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
 
-lemmas sb_dec_lem = int_mod_le' 
-  [where n = "2 ^ (Suc ?k)" and b = "?a + 2 ^ ?k", 
-  simplified zless2p, OF _ TrueI, simplified]
+lemma sb_dec_lem:
+  "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
+  by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
+    simplified zless2p, OF _ TrueI, simplified])
 
-lemmas sb_dec_lem' = iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]
+lemma sb_dec_lem':
+  "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
+  by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified])
 
 lemma sbintrunc_dec:
   "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
 
-lemmas zmod_uminus' = zmod_uminus [where b="?c"]
-lemmas zpower_zmod' = zpower_zmod [where m="?c" and y="?k"]
+lemmas zmod_uminus' = zmod_uminus [where b="c", standard]
+lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
 
 lemmas brdmod1s' [symmetric] = 
   zmod_zadd_left_eq zmod_zadd_right_eq 
@@ -539,11 +545,11 @@
   zmod_zsub_left_eq [where b = "1"]
 
 lemmas bintr_arith1s =
-  brdmod1s' [where c="2^?n", folded pred_def succ_def bintrunc_mod2p]
+  brdmod1s' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
 lemmas bintr_ariths =
-  brdmods' [where c="2^?n", folded pred_def succ_def bintrunc_mod2p]
+  brdmods' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
 
-lemmas m2pths [OF zless2p, standard] = pos_mod_sign pos_mod_bound
+lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard] 
 
 lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
   by (simp add : no_bintr m2pths)
@@ -666,14 +672,14 @@
 lemmas replicate_pred_simp [simp] =
   replicate_minus_simp [of "number_of bin", simplified nobm1, standard]
 
-lemmas power_Suc_no [simp] = power_Suc [of "number_of ?a"]
+lemmas power_Suc_no [simp] = power_Suc [of "number_of a", standard]
 
 lemmas power_minus_simp = 
   trans [OF gen_minus [where f = "power f"] power_Suc, standard]
 
 lemmas power_pred_simp = 
   power_minus_simp [of "number_of bin", simplified nobm1, standard]
-lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of ?f"]
+lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f", standard]
 
 lemma list_exhaust_size_gt0:
   assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
diff -r 510b46987886 -r 0d46bea01741 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Thu Nov 08 20:07:58 2007 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Thu Nov 08 20:08:00 2007 +0100
@@ -288,9 +288,9 @@
   apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])
   done
 
-lemmas zmod_zsub_left_eq = 
-  zmod_zadd_left_eq [where b = "- ?b", simplified diff_int_def [symmetric]]
-  
+lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
+  by (rule zmod_zadd_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
+
 lemma zmod_zsub_self [simp]: 
   "((b :: int) - a) mod a = b mod a"
   by (simp add: zmod_zsub_right_eq)
@@ -378,7 +378,8 @@
    apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a])
   done
 
-lemmas int_mod_le' = int_mod_le [where a = "?b - ?n", simplified]
+lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
+  by (rule int_mod_le [where a = "b - n" and n = n, simplified])
 
 lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
   apply (cases "0 <= a")
@@ -389,7 +390,8 @@
   apply assumption
   done
 
-lemmas int_mod_ge' = int_mod_ge [where a = "?b + ?n", simplified]
+lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n"
+  by (rule int_mod_ge [where a = "b + n" and n = n, simplified])
 
 lemma mod_add_if_z:
   "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
diff -r 510b46987886 -r 0d46bea01741 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Thu Nov 08 20:07:58 2007 +0100
+++ b/src/HOL/Word/WordDefinition.thy	Thu Nov 08 20:08:00 2007 +0100
@@ -402,7 +402,7 @@
     bin_to_bl (len_of TYPE('a)) o uint"
   by (auto simp: to_bl_def intro: ext)
 
-lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of ?w"]
+lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of w", standard]
 
 lemmas uints_mod = uints_def [unfolded no_bintr_alt1]
 
@@ -673,8 +673,7 @@
   done
 
 lemma unats_uints: "unats n = nat ` uints n"
-  apply (auto simp add : uints_unats image_iff)
-  done
+  by (auto simp add : uints_unats image_iff)
 
 lemmas bintr_num = word_ubin.norm_eq_iff 
   [symmetric, folded word_number_of_def, standard]
diff -r 510b46987886 -r 0d46bea01741 src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Thu Nov 08 20:07:58 2007 +0100
+++ b/src/HOL/Word/WordGenLib.thy	Thu Nov 08 20:08:00 2007 +0100
@@ -263,9 +263,9 @@
   by (simp add: unat_sub_if_size order_le_less word_less_nat_alt)
 
 lemmas word_less_sub1_numberof [simp] =
-  word_less_sub1 [of "number_of ?w"]
+  word_less_sub1 [of "number_of w", standard]
 lemmas word_le_sub1_numberof [simp] =
-  word_le_sub1 [of "number_of ?w"]
+  word_le_sub1 [of "number_of w", standard]
   
 lemma word_of_int_minus: 
   "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
@@ -396,7 +396,7 @@
  apply simp
 apply (case_tac "1 + (n - m) = 0")
  apply (simp add: word_rec_0)
- apply (rule arg_cong[where f="word_rec ?a ?b"])
+ apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
  apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
   apply simp
  apply (simp (no_asm_use))