--- a/src/HOL/Word/Bit_Representation.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,27 +1,24 @@
-(*
- Author: Jeremy Dawson, NICTA
-*)
+(* Title: HOL/Word/Bit_Representation.thy
+ Author: Jeremy Dawson, NICTA
+*)
section \<open>Integers as implict bit strings\<close>
theory Bit_Representation
-imports Misc_Numeric
+ imports Misc_Numeric
begin
subsection \<open>Constructors and destructors for binary integers\<close>
-definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
-where
- "k BIT b = (if b then 1 else 0) + k + k"
+definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
+ where "k BIT b = (if b then 1 else 0) + k + k"
-lemma Bit_B0:
- "k BIT False = k + k"
- by (unfold Bit_def) simp
+lemma Bit_B0: "k BIT False = k + k"
+ by (simp add: Bit_def)
-lemma Bit_B1:
- "k BIT True = k + k + 1"
- by (unfold Bit_def) simp
-
+lemma Bit_B1: "k BIT True = k + k + 1"
+ by (simp add: Bit_def)
+
lemma Bit_B0_2t: "k BIT False = 2 * k"
by (rule trans, rule Bit_B0) simp
@@ -29,36 +26,28 @@
by (rule trans, rule Bit_B1) simp
definition bin_last :: "int \<Rightarrow> bool"
-where
- "bin_last w \<longleftrightarrow> w mod 2 = 1"
+ where "bin_last w \<longleftrightarrow> w mod 2 = 1"
-lemma bin_last_odd:
- "bin_last = odd"
+lemma bin_last_odd: "bin_last = odd"
by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero)
definition bin_rest :: "int \<Rightarrow> int"
-where
- "bin_rest w = w div 2"
+ where "bin_rest w = w div 2"
-lemma bin_rl_simp [simp]:
- "bin_rest w BIT bin_last w = w"
+lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w"
unfolding bin_rest_def bin_last_def Bit_def
- using div_mult_mod_eq [of w 2]
- by (cases "w mod 2 = 0", simp_all)
+ by (cases "w mod 2 = 0") (use div_mult_mod_eq [of w 2] in simp_all)
lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
unfolding bin_rest_def Bit_def
- by (cases b, simp_all)
+ by (cases b) simp_all
lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b"
unfolding bin_last_def Bit_def
by (cases b) simp_all
lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
- apply (auto simp add: Bit_def)
- apply arith
- apply arith
- done
+ by (auto simp: Bit_def) arith+
lemma BIT_bin_simps [simp]:
"numeral k BIT False = numeral (Num.Bit0 k)"
@@ -66,34 +55,32 @@
"(- numeral k) BIT False = - numeral (Num.Bit0 k)"
"(- numeral k) BIT True = - numeral (Num.BitM k)"
unfolding numeral.simps numeral_BitM
- unfolding Bit_def
- by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
+ by (simp_all add: Bit_def del: arith_simps add_numeral_special diff_numeral_special)
lemma BIT_special_simps [simp]:
- shows "0 BIT False = 0" and "0 BIT True = 1"
- and "1 BIT False = 2" and "1 BIT True = 3"
- and "(- 1) BIT False = - 2" and "(- 1) BIT True = - 1"
- unfolding Bit_def by simp_all
+ shows "0 BIT False = 0"
+ and "0 BIT True = 1"
+ and "1 BIT False = 2"
+ and "1 BIT True = 3"
+ and "(- 1) BIT False = - 2"
+ and "(- 1) BIT True = - 1"
+ by (simp_all add: Bit_def)
lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b"
- apply (auto simp add: Bit_def)
- apply arith
- done
+ by (auto simp: Bit_def) arith
lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b"
- apply (auto simp add: Bit_def)
- apply arith
- done
+ by (auto simp: Bit_def) arith
lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
- by (induct w, simp_all)
+ by (induct w) simp_all
lemma expand_BIT:
"numeral (Num.Bit0 w) = numeral w BIT False"
"numeral (Num.Bit1 w) = numeral w BIT True"
"- numeral (Num.Bit0 w) = (- numeral w) BIT False"
"- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True"
- unfolding add_One by (simp_all add: BitM_inc)
+ by (simp_all add: add_One BitM_inc)
lemma bin_last_numeral_simps [simp]:
"\<not> bin_last 0"
@@ -117,13 +104,11 @@
"bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
by (simp_all add: bin_rest_def zdiv_zminus1_eq_if) (auto simp add: divmod_def)
-lemma less_Bits:
- "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
- unfolding Bit_def by auto
+lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
+ by (auto simp: Bit_def)
-lemma le_Bits:
- "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)"
- unfolding Bit_def by auto
+lemma le_Bits: "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)"
+ by (auto simp: Bit_def)
lemma pred_BIT_simps [simp]:
"x BIT False - 1 = (x - 1) BIT True"
@@ -148,31 +133,27 @@
"x BIT True * y = (x * y) BIT False + y"
by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
-lemma B_mod_2':
- "X = 2 ==> (w BIT True) mod X = 1 & (w BIT False) mod X = 0"
- apply (simp (no_asm) only: Bit_B0 Bit_B1)
- apply simp
- done
+lemma B_mod_2': "X = 2 \<Longrightarrow> (w BIT True) mod X = 1 \<and> (w BIT False) mod X = 0"
+ by (simp add: Bit_B0 Bit_B1)
-lemma bin_ex_rl: "EX w b. w BIT b = bin"
+lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
by (metis bin_rl_simp)
lemma bin_exhaust:
- assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
+ assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
shows "Q"
- apply (insert bin_ex_rl [of bin])
+ apply (insert bin_ex_rl [of bin])
apply (erule exE)+
- apply (rule Q)
+ apply (rule that)
apply force
done
-primrec bin_nth where
- Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
+primrec bin_nth
+ where
+ Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
| Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
-lemma bin_abs_lem:
- "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
- nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
+lemma bin_abs_lem: "bin = (w BIT b) \<Longrightarrow> bin \<noteq> -1 \<longrightarrow> bin \<noteq> 0 \<longrightarrow> nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
apply clarsimp
apply (unfold Bit_def)
apply (cases b)
@@ -183,10 +164,9 @@
lemma bin_induct:
assumes PPls: "P 0"
and PMin: "P (- 1)"
- and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
+ and PBit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)"
shows "P bin"
- apply (rule_tac P=P and a=bin and f1="nat o abs"
- in wf_measure [THEN wf_induct])
+ apply (rule_tac P=P and a=bin and f1="nat \<circ> abs" in wf_measure [THEN wf_induct])
apply (simp add: measure_def inv_image_def)
apply (case_tac x rule: bin_exhaust)
apply (frule bin_abs_lem)
@@ -196,26 +176,23 @@
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
-lemma bin_nth_eq_iff:
- "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
+lemma bin_nth_eq_iff: "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
proof -
- have bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y"
+ have bin_nth_lem [rule_format]: "\<forall>y. bin_nth x = bin_nth y \<longrightarrow> x = y"
apply (induct x rule: bin_induct)
apply safe
apply (erule rev_mp)
apply (induct_tac y rule: bin_induct)
apply safe
apply (drule_tac x=0 in fun_cong, force)
- apply (erule notE, rule ext,
- drule_tac x="Suc x" in fun_cong, force)
+ apply (erule notE, rule ext, drule_tac x="Suc x" in fun_cong, force)
apply (drule_tac x=0 in fun_cong, force)
apply (erule rev_mp)
apply (induct_tac y rule: bin_induct)
apply safe
apply (drule_tac x=0 in fun_cong, force)
- apply (erule notE, rule ext,
- drule_tac x="Suc x" in fun_cong, force)
- apply (metis Bit_eq_m1_iff Z bin_last_BIT)
+ apply (erule notE, rule ext, drule_tac x="Suc x" in fun_cong, force)
+ apply (metis Bit_eq_m1_iff Z bin_last_BIT)
apply (case_tac y rule: bin_exhaust)
apply clarify
apply (erule allE)
@@ -227,13 +204,12 @@
apply (drule_tac x="Suc x" for x in fun_cong, force)
done
show ?thesis
- by (auto elim: bin_nth_lem)
+ by (auto elim: bin_nth_lem)
qed
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]]
-lemma bin_eq_iff:
- "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
+lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
using bin_nth_eq_iff by auto
lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
@@ -251,11 +227,10 @@
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
by auto
-lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
+lemma bin_nth_minus [simp]: "0 < n \<Longrightarrow> bin_nth (w BIT b) n = bin_nth w (n - 1)"
by (cases n) auto
-lemma bin_nth_numeral:
- "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)"
+lemma bin_nth_numeral: "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)"
by (simp add: numeral_eq_Suc)
lemmas bin_nth_numeral_simps [simp] =
@@ -265,7 +240,7 @@
bin_nth_numeral [OF bin_rest_numeral_simps(7)]
bin_nth_numeral [OF bin_rest_numeral_simps(8)]
-lemmas bin_nth_simps =
+lemmas bin_nth_simps =
bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1
bin_nth_numeral_simps
@@ -273,8 +248,7 @@
subsection \<open>Truncating binary integers\<close>
definition bin_sign :: "int \<Rightarrow> int"
-where
- bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
+ where "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
lemma bin_sign_simps [simp]:
"bin_sign 0 = 0"
@@ -283,28 +257,26 @@
"bin_sign (numeral k) = 0"
"bin_sign (- numeral k) = -1"
"bin_sign (w BIT b) = bin_sign w"
- unfolding bin_sign_def Bit_def
- by simp_all
+ by (simp_all add: bin_sign_def Bit_def)
-lemma bin_sign_rest [simp]:
- "bin_sign (bin_rest w) = bin_sign w"
+lemma bin_sign_rest [simp]: "bin_sign (bin_rest w) = bin_sign w"
by (cases w rule: bin_exhaust) auto
-primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where
- Z : "bintrunc 0 bin = 0"
-| Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
+primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
+ where
+ Z : "bintrunc 0 bin = 0"
+ | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
-primrec sbintrunc :: "nat => int => int" where
- Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
-| Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
+primrec sbintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
+ where
+ Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
+ | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
by (induct n arbitrary: w) auto
-lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
- apply (induct n arbitrary: w, clarsimp)
- apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
- done
+lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n"
+ by (induct n arbitrary: w) (auto simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
apply (induct n arbitrary: w)
@@ -330,10 +302,8 @@
"bintrunc (Suc n) (- 1) = bintrunc n (- 1) BIT True"
"bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT False"
"bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True"
- "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
- bintrunc n (- numeral w) BIT False"
- "bintrunc (Suc n) (- numeral (Num.Bit1 w)) =
- bintrunc n (- numeral (w + Num.One)) BIT True"
+ "bintrunc (Suc n) (- numeral (Num.Bit0 w)) = bintrunc n (- numeral w) BIT False"
+ "bintrunc (Suc n) (- numeral (Num.Bit1 w)) = bintrunc n (- numeral (w + Num.One)) BIT True"
by simp_all
lemma sbintrunc_0_numeral [simp]:
@@ -346,14 +316,10 @@
lemma sbintrunc_Suc_numeral:
"sbintrunc (Suc n) 1 = 1"
- "sbintrunc (Suc n) (numeral (Num.Bit0 w)) =
- sbintrunc n (numeral w) BIT False"
- "sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
- sbintrunc n (numeral w) BIT True"
- "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) =
- sbintrunc n (- numeral w) BIT False"
- "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) =
- sbintrunc n (- numeral (w + Num.One)) BIT True"
+ "sbintrunc (Suc n) (numeral (Num.Bit0 w)) = sbintrunc n (numeral w) BIT False"
+ "sbintrunc (Suc n) (numeral (Num.Bit1 w)) = sbintrunc n (numeral w) BIT True"
+ "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) = sbintrunc n (- numeral w) BIT False"
+ "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) = sbintrunc n (- numeral (w + Num.One)) BIT True"
by simp_all
lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
@@ -361,24 +327,21 @@
apply (case_tac bin rule: bin_exhaust, case_tac b, auto)
done
-lemma nth_bintr: "bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
+lemma nth_bintr: "bin_nth (bintrunc m w) n \<longleftrightarrow> n < m \<and> bin_nth w n"
apply (induct n arbitrary: w m)
apply (case_tac m, auto)[1]
apply (case_tac m, auto)[1]
done
-lemma nth_sbintr:
- "bin_nth (sbintrunc m w) n =
- (if n < m then bin_nth w n else bin_nth w m)"
+lemma nth_sbintr: "bin_nth (sbintrunc m w) n = (if n < m then bin_nth w n else bin_nth w m)"
apply (induct n arbitrary: w m)
+ apply (case_tac m)
+ apply simp_all
apply (case_tac m)
- apply simp_all
- apply (case_tac m)
- apply simp_all
+ apply simp_all
done
-lemma bin_nth_Bit:
- "bin_nth (w BIT b) n = (n = 0 & b | (EX m. n = Suc m & bin_nth w m))"
+lemma bin_nth_Bit: "bin_nth (w BIT b) n \<longleftrightarrow> n = 0 \<and> b \<or> (\<exists>m. n = Suc m \<and> bin_nth w m)"
by (cases n) auto
lemma bin_nth_Bit0:
@@ -391,69 +354,58 @@
n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)"
using bin_nth_Bit [where w="numeral w" and b="True"] by simp
-lemma bintrunc_bintrunc_l:
- "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
- by (rule bin_eqI) (auto simp add : nth_bintr)
+lemma bintrunc_bintrunc_l: "n \<le> m \<Longrightarrow> bintrunc m (bintrunc n w) = bintrunc n w"
+ by (rule bin_eqI) (auto simp: nth_bintr)
-lemma sbintrunc_sbintrunc_l:
- "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
+lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> sbintrunc m (sbintrunc n w) = sbintrunc n w"
by (rule bin_eqI) (auto simp: nth_sbintr)
-lemma bintrunc_bintrunc_ge:
- "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
+lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> bintrunc n (bintrunc m w) = bintrunc n w"
by (rule bin_eqI) (auto simp: nth_bintr)
-lemma bintrunc_bintrunc_min [simp]:
- "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
- apply (rule bin_eqI)
- apply (auto simp: nth_bintr)
- done
+lemma bintrunc_bintrunc_min [simp]: "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
+ by (rule bin_eqI) (auto simp: nth_bintr)
-lemma sbintrunc_sbintrunc_min [simp]:
- "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
- apply (rule bin_eqI)
- apply (auto simp: nth_sbintr min.absorb1 min.absorb2)
- done
+lemma sbintrunc_sbintrunc_min [simp]: "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
+ by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2)
-lemmas bintrunc_Pls =
+lemmas bintrunc_Pls =
bintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-lemmas bintrunc_Min [simp] =
+lemmas bintrunc_Min [simp] =
bintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-lemmas bintrunc_BIT [simp] =
+lemmas bintrunc_BIT [simp] =
bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
bintrunc_Suc_numeral
-lemmas sbintrunc_Suc_Pls =
+lemmas sbintrunc_Suc_Pls =
sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-lemmas sbintrunc_Suc_Min =
+lemmas sbintrunc_Suc_Min =
sbintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-lemmas sbintrunc_Suc_BIT [simp] =
+lemmas sbintrunc_Suc_BIT [simp] =
sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
sbintrunc_Suc_numeral
-lemmas sbintrunc_Pls =
- sbintrunc.Z [where bin="0",
- simplified bin_last_numeral_simps bin_rest_numeral_simps]
+lemmas sbintrunc_Pls =
+ sbintrunc.Z [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-lemmas sbintrunc_Min =
- sbintrunc.Z [where bin="-1",
- simplified bin_last_numeral_simps bin_rest_numeral_simps]
+lemmas sbintrunc_Min =
+ sbintrunc.Z [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
-lemmas sbintrunc_0_BIT_B0 [simp] =
- sbintrunc.Z [where bin="w BIT False",
- simplified bin_last_numeral_simps bin_rest_numeral_simps] for w
+lemmas sbintrunc_0_BIT_B0 [simp] =
+ sbintrunc.Z [where bin="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+ for w
-lemmas sbintrunc_0_BIT_B1 [simp] =
- sbintrunc.Z [where bin="w BIT True",
- simplified bin_last_BIT bin_rest_numeral_simps] for w
+lemmas sbintrunc_0_BIT_B1 [simp] =
+ sbintrunc.Z [where bin="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
+ for w
lemmas sbintrunc_0_simps =
sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
@@ -461,20 +413,18 @@
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
-lemma bintrunc_minus:
- "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w"
+lemma bintrunc_minus: "0 < n \<Longrightarrow> bintrunc (Suc (n - 1)) w = bintrunc n w"
+ by auto
+
+lemma sbintrunc_minus: "0 < n \<Longrightarrow> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
by auto
-lemma sbintrunc_minus:
- "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
- by auto
-
-lemmas bintrunc_minus_simps =
+lemmas bintrunc_minus_simps =
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]]
-lemmas sbintrunc_minus_simps =
+lemmas sbintrunc_minus_simps =
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]]
-lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
+lemmas thobini1 = arg_cong [where f = "\<lambda>w. w BIT b"] for b
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
@@ -484,35 +434,31 @@
lemmas bintrunc_Min_minus_I = bmsts(2)
lemmas bintrunc_BIT_minus_I = bmsts(3)
-lemma bintrunc_Suc_lem:
- "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
+lemma bintrunc_Suc_lem: "bintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> bintrunc m x = y"
by auto
-lemmas bintrunc_Suc_Ialts =
+lemmas bintrunc_Suc_Ialts =
bintrunc_Min_I [THEN bintrunc_Suc_lem]
bintrunc_BIT_I [THEN bintrunc_Suc_lem]
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
-lemmas sbintrunc_Suc_Is =
+lemmas sbintrunc_Suc_Is =
sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans]]
-lemmas sbintrunc_Suc_minus_Is =
+lemmas sbintrunc_Suc_minus_Is =
sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]]
-lemma sbintrunc_Suc_lem:
- "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
+lemma sbintrunc_Suc_lem: "sbintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> sbintrunc m x = y"
by auto
-lemmas sbintrunc_Suc_Ialts =
+lemmas sbintrunc_Suc_Ialts =
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem]
-lemma sbintrunc_bintrunc_lt:
- "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"
+lemma sbintrunc_bintrunc_lt: "m > n \<Longrightarrow> sbintrunc n (bintrunc m w) = sbintrunc n w"
by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
-lemma bintrunc_sbintrunc_le:
- "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"
+lemma bintrunc_sbintrunc_le: "m \<le> Suc n \<Longrightarrow> bintrunc m (sbintrunc n w) = bintrunc m w"
apply (rule bin_eqI)
apply (auto simp: nth_sbintr nth_bintr)
apply (subgoal_tac "x=n", safe, arith+)[1]
@@ -522,19 +468,15 @@
lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]
lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]
-lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l]
+lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l]
-lemma bintrunc_sbintrunc' [simp]:
- "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
+lemma bintrunc_sbintrunc' [simp]: "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
by (cases n) (auto simp del: bintrunc.Suc)
-lemma sbintrunc_bintrunc' [simp]:
- "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
+lemma sbintrunc_bintrunc' [simp]: "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
by (cases n) (auto simp del: bintrunc.Suc)
-lemma bin_sbin_eq_iff:
- "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow>
- sbintrunc n x = sbintrunc n y"
+lemma bin_sbin_eq_iff: "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> sbintrunc n x = sbintrunc n y"
apply (rule iffI)
apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
apply simp
@@ -543,8 +485,7 @@
done
lemma bin_sbin_eq_iff':
- "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow>
- sbintrunc (n - 1) x = sbintrunc (n - 1) y"
+ "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> sbintrunc (n - 1) x = sbintrunc (n - 1) y"
by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
@@ -557,36 +498,29 @@
tends to get applied where it's not wanted in developing the theories,
we get a version for when the word length is given literally *)
-lemmas nat_non0_gr =
+lemmas nat_non0_gr =
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl]
lemma bintrunc_numeral:
- "bintrunc (numeral k) x =
- bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+ "bintrunc (numeral k) x = bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
by (simp add: numeral_eq_Suc)
lemma sbintrunc_numeral:
- "sbintrunc (numeral k) x =
- sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+ "sbintrunc (numeral k) x = sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
by (simp add: numeral_eq_Suc)
lemma bintrunc_numeral_simps [simp]:
- "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
- bintrunc (pred_numeral k) (numeral w) BIT False"
- "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
- bintrunc (pred_numeral k) (numeral w) BIT True"
- "bintrunc (numeral k) (- numeral (Num.Bit0 w)) =
- bintrunc (pred_numeral k) (- numeral w) BIT False"
+ "bintrunc (numeral k) (numeral (Num.Bit0 w)) = bintrunc (pred_numeral k) (numeral w) BIT False"
+ "bintrunc (numeral k) (numeral (Num.Bit1 w)) = bintrunc (pred_numeral k) (numeral w) BIT True"
+ "bintrunc (numeral k) (- numeral (Num.Bit0 w)) = bintrunc (pred_numeral k) (- numeral w) BIT False"
"bintrunc (numeral k) (- numeral (Num.Bit1 w)) =
bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True"
"bintrunc (numeral k) 1 = 1"
by (simp_all add: bintrunc_numeral)
lemma sbintrunc_numeral_simps [simp]:
- "sbintrunc (numeral k) (numeral (Num.Bit0 w)) =
- sbintrunc (pred_numeral k) (numeral w) BIT False"
- "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
- sbintrunc (pred_numeral k) (numeral w) BIT True"
+ "sbintrunc (numeral k) (numeral (Num.Bit0 w)) = sbintrunc (pred_numeral k) (numeral w) BIT False"
+ "sbintrunc (numeral k) (numeral (Num.Bit1 w)) = sbintrunc (pred_numeral k) (numeral w) BIT True"
"sbintrunc (numeral k) (- numeral (Num.Bit0 w)) =
sbintrunc (pred_numeral k) (- numeral w) BIT False"
"sbintrunc (numeral k) (- numeral (Num.Bit1 w)) =
@@ -597,49 +531,45 @@
lemma no_bintr_alt1: "bintrunc n = (\<lambda>w. w mod 2 ^ n :: int)"
by (rule ext) (rule bintrunc_mod2p)
-lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"
+lemma range_bintrunc: "range (bintrunc n) = {i. 0 \<le> i \<and> i < 2 ^ n}"
apply (unfold no_bintr_alt1)
apply (auto simp add: image_iff)
apply (rule exI)
apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
done
-lemma no_sbintr_alt2:
- "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
+lemma no_sbintr_alt2: "sbintrunc n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
by (rule ext) (simp add : sbintrunc_mod2p)
-lemma range_sbintrunc:
- "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
+lemma range_sbintrunc: "range (sbintrunc n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}"
apply (unfold no_sbintr_alt2)
apply (auto simp add: image_iff eq_diff_eq)
apply (rule exI)
apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
done
-lemma sb_inc_lem:
- "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+ for a :: int
apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
apply (rule TrueI)
done
-lemma sb_inc_lem':
- "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+ for a :: int
by (rule sb_inc_lem) simp
-lemma sbintrunc_inc:
- "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
+lemma sbintrunc_inc: "x < - (2^n) \<Longrightarrow> x + 2^(Suc n) \<le> sbintrunc n x"
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
-lemma sb_dec_lem:
- "(0::int) \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+ for a :: int
using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
-lemma sb_dec_lem':
- "(2::int) ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+ for a :: int
by (rule sb_dec_lem) simp
-lemma sbintrunc_dec:
- "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
+lemma sbintrunc_dec: "x \<ge> (2 ^ n) \<Longrightarrow> x - 2 ^ (Suc n) >= sbintrunc n x"
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
@@ -659,55 +589,48 @@
lemma sbintr_lt: "sbintrunc n w < 2 ^ n"
by (simp add: sbintrunc_mod2p)
-lemma sign_Pls_ge_0:
- "(bin_sign bin = 0) = (bin >= (0 :: int))"
- unfolding bin_sign_def by simp
+lemma sign_Pls_ge_0: "bin_sign bin = 0 \<longleftrightarrow> bin \<ge> 0"
+ for bin :: int
+ by (simp add: bin_sign_def)
-lemma sign_Min_lt_0:
- "(bin_sign bin = -1) = (bin < (0 :: int))"
- unfolding bin_sign_def by simp
+lemma sign_Min_lt_0: "bin_sign bin = -1 \<longleftrightarrow> bin < 0"
+ for bin :: int
+ by (simp add: bin_sign_def)
-lemma bin_rest_trunc:
- "(bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
+lemma bin_rest_trunc: "bin_rest (bintrunc n bin) = bintrunc (n - 1) (bin_rest bin)"
by (induct n arbitrary: bin) auto
lemma bin_rest_power_trunc:
- "(bin_rest ^^ k) (bintrunc n bin) =
- bintrunc (n - k) ((bin_rest ^^ k) bin)"
+ "(bin_rest ^^ k) (bintrunc n bin) = bintrunc (n - k) ((bin_rest ^^ k) bin)"
by (induct k) (auto simp: bin_rest_trunc)
-lemma bin_rest_trunc_i:
- "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
+lemma bin_rest_trunc_i: "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
by auto
-lemma bin_rest_strunc:
- "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
+lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
by (induct n arbitrary: bin) auto
-lemma bintrunc_rest [simp]:
- "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
- apply (induct n arbitrary: bin, simp)
+lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
+ apply (induct n arbitrary: bin)
+ apply simp
apply (case_tac bin rule: bin_exhaust)
apply (auto simp: bintrunc_bintrunc_l)
done
-lemma sbintrunc_rest [simp]:
- "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
- apply (induct n arbitrary: bin, simp)
+lemma sbintrunc_rest [simp]: "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
+ apply (induct n arbitrary: bin)
+ apply simp
apply (case_tac bin rule: bin_exhaust)
apply (auto simp: bintrunc_bintrunc_l split: bool.splits)
done
-lemma bintrunc_rest':
- "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"
+lemma bintrunc_rest': "bintrunc n \<circ> bin_rest \<circ> bintrunc n = bin_rest \<circ> bintrunc n"
by (rule ext) auto
-lemma sbintrunc_rest' :
- "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"
+lemma sbintrunc_rest': "sbintrunc n \<circ> bin_rest \<circ> sbintrunc n = bin_rest \<circ> sbintrunc n"
by (rule ext) auto
-lemma rco_lem:
- "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f"
+lemma rco_lem: "f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f"
apply (rule ext)
apply (induct_tac n)
apply (simp_all (no_asm))
@@ -717,27 +640,29 @@
apply simp
done
-lemmas rco_bintr = bintrunc_rest'
+lemmas rco_bintr = bintrunc_rest'
[THEN rco_lem [THEN fun_cong], unfolded o_def]
-lemmas rco_sbintr = sbintrunc_rest'
+lemmas rco_sbintr = sbintrunc_rest'
[THEN rco_lem [THEN fun_cong], unfolded o_def]
-
+
subsection \<open>Splitting and concatenation\<close>
-primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
- Z: "bin_split 0 w = (w, 0)"
- | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
- in (w1, w2 BIT bin_last w))"
+primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int"
+ where
+ Z: "bin_split 0 w = (w, 0)"
+ | Suc: "bin_split (Suc n) w =
+ (let (w1, w2) = bin_split n (bin_rest w)
+ in (w1, w2 BIT bin_last w))"
lemma [code]:
"bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))"
"bin_split 0 w = (w, 0)"
by simp_all
-primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
- Z: "bin_cat w 0 v = w"
+primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int"
+ where
+ Z: "bin_cat w 0 v = w"
| Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
end
-
--- a/src/HOL/Word/Bits.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bits.thy Mon Apr 03 23:12:44 2017 +0200
@@ -5,35 +5,32 @@
section \<open>Syntactic classes for bitwise operations\<close>
theory Bits
-imports Main
+ imports Main
begin
class bit =
- fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
- and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
- and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
- and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
+ fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
+ and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
+ and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
+ and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
text \<open>
We want the bitwise operations to bind slightly weaker
- than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
+ than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
bind slightly stronger than \<open>*\<close>.
\<close>
-text \<open>
- Testing and shifting operations.
-\<close>
+text \<open>Testing and shifting operations.\<close>
class bits = bit +
- fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
- and lsb :: "'a \<Rightarrow> bool"
- and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
- and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
- and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
- and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
+ fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
+ and lsb :: "'a \<Rightarrow> bool"
+ and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
+ and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
+ and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
+ and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
class bitss = bits +
- fixes msb :: "'a \<Rightarrow> bool"
+ fixes msb :: "'a \<Rightarrow> bool"
end
-
--- a/src/HOL/Word/Bits_Bit.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bits_Bit.thy Mon Apr 03 23:12:44 2017 +0200
@@ -11,20 +11,24 @@
instantiation bit :: bit
begin
-primrec bitNOT_bit where
- "NOT 0 = (1::bit)"
+primrec bitNOT_bit
+ where
+ "NOT 0 = (1::bit)"
| "NOT 1 = (0::bit)"
-primrec bitAND_bit where
- "0 AND y = (0::bit)"
+primrec bitAND_bit
+ where
+ "0 AND y = (0::bit)"
| "1 AND y = (y::bit)"
-primrec bitOR_bit where
- "0 OR y = (y::bit)"
+primrec bitOR_bit
+ where
+ "0 OR y = (y::bit)"
| "1 OR y = (1::bit)"
-primrec bitXOR_bit where
- "0 XOR y = (y::bit)"
+primrec bitXOR_bit
+ where
+ "0 XOR y = (y::bit)"
| "1 XOR y = (NOT y :: bit)"
instance ..
@@ -34,40 +38,48 @@
lemmas bit_simps =
bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
-lemma bit_extra_simps [simp]:
- "x AND 0 = (0::bit)"
- "x AND 1 = (x::bit)"
- "x OR 1 = (1::bit)"
- "x OR 0 = (x::bit)"
- "x XOR 1 = NOT (x::bit)"
- "x XOR 0 = (x::bit)"
+lemma bit_extra_simps [simp]:
+ "x AND 0 = 0"
+ "x AND 1 = x"
+ "x OR 1 = 1"
+ "x OR 0 = x"
+ "x XOR 1 = NOT x"
+ "x XOR 0 = x"
+ for x :: bit
by (cases x, auto)+
-lemma bit_ops_comm:
- "(x::bit) AND y = y AND x"
- "(x::bit) OR y = y OR x"
- "(x::bit) XOR y = y XOR x"
+lemma bit_ops_comm:
+ "x AND y = y AND x"
+ "x OR y = y OR x"
+ "x XOR y = y XOR x"
+ for x :: bit
by (cases y, auto)+
-lemma bit_ops_same [simp]:
- "(x::bit) AND x = x"
- "(x::bit) OR x = x"
- "(x::bit) XOR x = 0"
+lemma bit_ops_same [simp]:
+ "x AND x = x"
+ "x OR x = x"
+ "x XOR x = 0"
+ for x :: bit
by (cases x, auto)+
-lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
+lemma bit_not_not [simp]: "NOT (NOT x) = x"
+ for x :: bit
by (cases x) auto
-lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
- by (induct b, simp_all)
+lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
+ for b c :: bit
+ by (induct b) simp_all
-lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
- by (induct b, simp_all)
+lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
+ for b c :: bit
+ by (induct b) simp_all
-lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
- by (induct b, simp_all)
+lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
+ for b :: bit
+ by (induct b) simp_all
-lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
- by (induct a, simp_all)
+lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
+ for a b :: bit
+ by (induct a) simp_all
end
--- a/src/HOL/Word/Bits_Int.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bits_Int.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,15 +1,15 @@
-(*
- Author: Jeremy Dawson and Gerwin Klein, NICTA
+(* Title: HOL/Word/Bits_Int.thy
+ Author: Jeremy Dawson and Gerwin Klein, NICTA
- Definitions and basic theorems for bit-wise logical operations
- for integers expressed using Pls, Min, BIT,
- and converting them to and from lists of bools.
-*)
+Definitions and basic theorems for bit-wise logical operations
+for integers expressed using Pls, Min, BIT,
+and converting them to and from lists of bools.
+*)
section \<open>Bitwise Operations on Binary Integers\<close>
theory Bits_Int
-imports Bits Bit_Representation
+ imports Bits Bit_Representation
begin
subsection \<open>Logical operations\<close>
@@ -19,17 +19,16 @@
instantiation int :: bit
begin
-definition int_not_def:
- "bitNOT = (\<lambda>x::int. - x - 1)"
+definition int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)"
-function bitAND_int where
- "bitAND_int x y =
- (if x = 0 then 0 else if x = -1 then y else
- (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
+function bitAND_int
+ where "bitAND_int x y =
+ (if x = 0 then 0 else if x = -1 then y
+ else (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
by pat_completeness simp
termination
- by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
+ by (relation "measure (nat \<circ> abs \<circ> fst)", simp_all add: bin_rest_def)
declare bitAND_int.simps [simp del]
@@ -67,8 +66,8 @@
lemma int_and_m1 [simp]: "(-1::int) AND x = x"
by (simp add: bitAND_int.simps)
-lemma int_and_Bits [simp]:
- "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
+lemma int_and_Bits [simp]:
+ "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
lemma int_or_zero [simp]: "(0::int) OR x = x"
@@ -77,14 +76,14 @@
lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
unfolding int_or_def by simp
-lemma int_or_Bits [simp]:
+lemma int_or_Bits [simp]:
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
unfolding int_or_def by simp
lemma int_xor_zero [simp]: "(0::int) XOR x = x"
unfolding int_xor_def by simp
-lemma int_xor_Bits [simp]:
+lemma int_xor_Bits [simp]:
"(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
unfolding int_xor_def by auto
@@ -115,9 +114,9 @@
by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
lemma bin_nth_ops:
- "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
+ "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
"!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
- "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
+ "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
"!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
by (induct n) auto
@@ -150,18 +149,18 @@
by (auto simp add: bin_eq_iff bin_nth_ops)
lemma bin_ops_same [simp]:
- "(x::int) AND x = x"
- "(x::int) OR x = x"
+ "(x::int) AND x = x"
+ "(x::int) OR x = x"
"(x::int) XOR x = 0"
by (auto simp add: bin_eq_iff bin_nth_ops)
-lemmas bin_log_esimps =
+lemmas bin_log_esimps =
int_and_extra_simps int_or_extra_simps int_xor_extra_simps
int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
(* basic properties of logical (bit-wise) operations *)
-lemma bbw_ao_absorb:
+lemma bbw_ao_absorb:
"!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
by (auto simp add: bin_eq_iff bin_nth_ops)
@@ -174,7 +173,7 @@
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
lemma int_xor_not:
- "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
+ "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
x XOR (NOT y) = NOT (x XOR y)"
by (auto simp add: bin_eq_iff bin_nth_ops)
@@ -193,30 +192,30 @@
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
(* BH: Why are these declared as simp rules??? *)
-lemma bbw_lcs [simp]:
+lemma bbw_lcs [simp]:
"(y::int) AND (x AND z) = x AND (y AND z)"
"(y::int) OR (x OR z) = x OR (y OR z)"
- "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
+ "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
by (auto simp add: bin_eq_iff bin_nth_ops)
-lemma bbw_not_dist:
- "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
+lemma bbw_not_dist:
+ "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
"!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
by (auto simp add: bin_eq_iff bin_nth_ops)
-lemma bbw_oa_dist:
- "!!y z::int. (x AND y) OR z =
+lemma bbw_oa_dist:
+ "!!y z::int. (x AND y) OR z =
(x OR z) AND (y OR z)"
by (auto simp add: bin_eq_iff bin_nth_ops)
-lemma bbw_ao_dist:
- "!!y z::int. (x OR y) AND z =
+lemma bbw_ao_dist:
+ "!!y z::int. (x OR y) AND z =
(x AND z) OR (y AND z)"
by (auto simp add: bin_eq_iff bin_nth_ops)
(*
Why were these declared simp???
-declare bin_ops_comm [simp] bbw_assocs [simp]
+declare bin_ops_comm [simp] bbw_assocs [simp]
*)
subsubsection \<open>Simplification with numerals\<close>
@@ -360,17 +359,17 @@
subsubsection \<open>Truncating results of bit-wise operations\<close>
-lemma bin_trunc_ao:
- "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
+lemma bin_trunc_ao:
+ "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
"!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
-lemma bin_trunc_xor:
- "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
+lemma bin_trunc_xor:
+ "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
bintrunc n (x XOR y)"
by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
-lemma bin_trunc_not:
+lemma bin_trunc_not:
"!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
@@ -392,26 +391,26 @@
Z: "bin_sc 0 b w = bin_rest w BIT b"
| Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
-lemma bin_nth_sc [simp]:
+lemma bin_nth_sc [simp]:
"bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
by (induct n arbitrary: w) auto
-lemma bin_sc_sc_same [simp]:
+lemma bin_sc_sc_same [simp]:
"bin_sc n c (bin_sc n b w) = bin_sc n c w"
by (induct n arbitrary: w) auto
lemma bin_sc_sc_diff:
- "m ~= n ==>
+ "m ~= n ==>
bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
apply (induct n arbitrary: w m)
apply (case_tac [!] m)
apply auto
done
-lemma bin_nth_sc_gen:
+lemma bin_nth_sc_gen:
"bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
by (induct n arbitrary: w m) (case_tac [!] m, auto)
-
+
lemma bin_sc_nth [simp]:
"(bin_sc n (bin_nth w n) w) = w"
by (induct n arbitrary: w) auto
@@ -419,8 +418,8 @@
lemma bin_sign_sc [simp]:
"bin_sign (bin_sc n b w) = bin_sign w"
by (induct n arbitrary: w) auto
-
-lemma bin_sc_bintr [simp]:
+
+lemma bin_sc_bintr [simp]:
"bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
apply (induct n arbitrary: w m)
apply (case_tac [!] w rule: bin_exhaust)
@@ -464,14 +463,14 @@
lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
by (induct n) auto
-
+
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
lemma bin_sc_minus:
"0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
by auto
-lemmas bin_sc_Suc_minus =
+lemmas bin_sc_Suc_minus =
trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
lemma bin_sc_numeral [simp]:
@@ -490,7 +489,7 @@
where
"bin_rsplit_aux n m c bs =
(if m = 0 | n = 0 then bs else
- let (a, b) = bin_split n c
+ let (a, b) = bin_split n c
in bin_rsplit_aux n (m - n) a (b # bs))"
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
@@ -501,7 +500,7 @@
where
"bin_rsplitl_aux n m c bs =
(if m = 0 | n = 0 then bs else
- let (a, b) = bin_split (min m n) c
+ let (a, b) = bin_split (min m n) c
in bin_rsplitl_aux n (m - n) a (b # bs))"
definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
@@ -511,7 +510,7 @@
declare bin_rsplit_aux.simps [simp del]
declare bin_rsplitl_aux.simps [simp del]
-lemma bin_sign_cat:
+lemma bin_sign_cat:
"bin_sign (bin_cat x n y) = bin_sign x"
by (induct n arbitrary: y) auto
@@ -519,8 +518,8 @@
"bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
by auto
-lemma bin_nth_cat:
- "bin_nth (bin_cat x k y) n =
+lemma bin_nth_cat:
+ "bin_nth (bin_cat x k y) n =
(if n < k then bin_nth y n else bin_nth x (n - k))"
apply (induct k arbitrary: n y)
apply clarsimp
@@ -528,8 +527,8 @@
done
lemma bin_nth_split:
- "bin_split n c = (a, b) ==>
- (ALL k. bin_nth a k = bin_nth c (n + k)) &
+ "bin_split n c = (a, b) ==>
+ (ALL k. bin_nth a k = bin_nth c (n + k)) &
(ALL k. bin_nth b k = (k < n & bin_nth c k))"
apply (induct n arbitrary: b c)
apply clarsimp
@@ -538,8 +537,8 @@
apply auto
done
-lemma bin_cat_assoc:
- "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
+lemma bin_cat_assoc:
+ "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
by (induct n arbitrary: z) auto
lemma bin_cat_assoc_sym:
@@ -551,23 +550,23 @@
lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
by (induct n arbitrary: w) auto
-lemma bintr_cat1:
+lemma bintr_cat1:
"bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
by (induct n arbitrary: b) auto
-
-lemma bintr_cat: "bintrunc m (bin_cat a n b) =
+
+lemma bintr_cat: "bintrunc m (bin_cat a n b) =
bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
-
-lemma bintr_cat_same [simp]:
+
+lemma bintr_cat_same [simp]:
"bintrunc n (bin_cat a n b) = bintrunc n b"
by (auto simp add : bintr_cat)
-lemma cat_bintr [simp]:
+lemma cat_bintr [simp]:
"bin_cat a n (bintrunc n b) = bin_cat a n b"
by (induct n arbitrary: b) auto
-lemma split_bintrunc:
+lemma split_bintrunc:
"bin_split n c = (a, b) ==> b = bintrunc n c"
by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
@@ -587,7 +586,7 @@
by (induct n) auto
lemma bin_split_trunc:
- "bin_split (min m n) c = (a, b) ==>
+ "bin_split (min m n) c = (a, b) ==>
bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
apply (induct n arbitrary: m b c, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
@@ -596,7 +595,7 @@
done
lemma bin_split_trunc1:
- "bin_split n c = (a, b) ==>
+ "bin_split n c = (a, b) ==>
bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
apply (induct n arbitrary: m b c, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
@@ -621,12 +620,12 @@
subsection \<open>Miscellaneous lemmas\<close>
-lemma nth_2p_bin:
+lemma nth_2p_bin:
"bin_nth (2 ^ n) m = (m = n)"
apply (induct n arbitrary: m)
apply clarsimp
apply safe
- apply (case_tac m)
+ apply (case_tac m)
apply (auto simp: Bit_B0_2t [symmetric])
done
--- a/src/HOL/Word/Bool_List_Representation.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,177 +1,156 @@
-(*
- Author: Jeremy Dawson, NICTA
+(* Title: HOL/Word/Bool_List_Representation.thy
+ Author: Jeremy Dawson, NICTA
- Theorems to do with integers, expressed using Pls, Min, BIT,
- theorems linking them to lists of booleans, and repeated splitting
- and concatenation.
-*)
+Theorems to do with integers, expressed using Pls, Min, BIT,
+theorems linking them to lists of booleans, and repeated splitting
+and concatenation.
+*)
section "Bool lists and integers"
theory Bool_List_Representation
-imports Main Bits_Int
+ imports Bits_Int
begin
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
-where
- "map2 f as bs = map (case_prod f) (zip as bs)"
+ where "map2 f as bs = map (case_prod f) (zip as bs)"
-lemma map2_Nil [simp, code]:
- "map2 f [] ys = []"
- unfolding map2_def by auto
+lemma map2_Nil [simp, code]: "map2 f [] ys = []"
+ by (auto simp: map2_def)
-lemma map2_Nil2 [simp, code]:
- "map2 f xs [] = []"
- unfolding map2_def by auto
+lemma map2_Nil2 [simp, code]: "map2 f xs [] = []"
+ by (auto simp: map2_def)
-lemma map2_Cons [simp, code]:
- "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
- unfolding map2_def by auto
+lemma map2_Cons [simp, code]: "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
+ by (auto simp: map2_def)
subsection \<open>Operations on lists of booleans\<close>
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
-where
- Nil: "bl_to_bin_aux [] w = w"
- | Cons: "bl_to_bin_aux (b # bs) w =
- bl_to_bin_aux bs (w BIT b)"
+ where
+ Nil: "bl_to_bin_aux [] w = w"
+ | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (w BIT b)"
definition bl_to_bin :: "bool list \<Rightarrow> int"
-where
- bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
+ where "bl_to_bin bs = bl_to_bin_aux bs 0"
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
-where
- Z: "bin_to_bl_aux 0 w bl = bl"
- | Suc: "bin_to_bl_aux (Suc n) w bl =
- bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
+ where
+ Z: "bin_to_bl_aux 0 w bl = bl"
+ | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
-where
- bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
+ where "bin_to_bl n w = bin_to_bl_aux n w []"
primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
-where
- Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+ where
+ Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
| Z: "bl_of_nth 0 f = []"
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- Z: "takefill fill 0 xs = []"
- | Suc: "takefill fill (Suc n) xs = (
- case xs of [] => fill # takefill fill n xs
- | y # ys => y # takefill fill n ys)"
+ Z: "takefill fill 0 xs = []"
+ | Suc: "takefill fill (Suc n) xs =
+ (case xs of
+ [] \<Rightarrow> fill # takefill fill n xs
+ | y # ys \<Rightarrow> y # takefill fill n ys)"
subsection "Arithmetic in terms of bool lists"
text \<open>
Arithmetic operations in terms of the reversed bool list,
- assuming input list(s) the same length, and don't extend them.
+ assuming input list(s) the same length, and don't extend them.
\<close>
-primrec rbl_succ :: "bool list => bool list"
-where
- Nil: "rbl_succ Nil = Nil"
+primrec rbl_succ :: "bool list \<Rightarrow> bool list"
+ where
+ Nil: "rbl_succ Nil = Nil"
| Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-primrec rbl_pred :: "bool list => bool list"
-where
- Nil: "rbl_pred Nil = Nil"
+primrec rbl_pred :: "bool list \<Rightarrow> bool list"
+ where
+ Nil: "rbl_pred Nil = Nil"
| Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-primrec rbl_add :: "bool list => bool list => bool list"
-where
- \<comment> "result is length of first arg, second arg may be longer"
- Nil: "rbl_add Nil x = Nil"
- | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
- (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
+primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+ where \<comment> "result is length of first arg, second arg may be longer"
+ Nil: "rbl_add Nil x = Nil"
+ | Cons: "rbl_add (y # ys) x =
+ (let ws = rbl_add ys (tl x)
+ in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
-primrec rbl_mult :: "bool list => bool list => bool list"
-where
- \<comment> "result is length of first arg, second arg may be longer"
- Nil: "rbl_mult Nil x = Nil"
- | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
- if y then rbl_add ws x else ws)"
+primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+ where \<comment> "result is length of first arg, second arg may be longer"
+ Nil: "rbl_mult Nil x = Nil"
+ | Cons: "rbl_mult (y # ys) x =
+ (let ws = False # rbl_mult ys x
+ in if y then rbl_add ws x else ws)"
-lemma butlast_power:
- "(butlast ^^ n) bl = take (length bl - n) bl"
+lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
by (induct n) (auto simp: butlast_take)
lemma bin_to_bl_aux_zero_minus_simp [simp]:
- "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl =
- bin_to_bl_aux (n - 1) 0 (False # bl)"
+ "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
by (cases n) auto
lemma bin_to_bl_aux_minus1_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (- 1) bl =
- bin_to_bl_aux (n - 1) (- 1) (True # bl)"
+ "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
by (cases n) auto
lemma bin_to_bl_aux_one_minus_simp [simp]:
- "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl =
- bin_to_bl_aux (n - 1) 0 (True # bl)"
+ "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
by (cases n) auto
lemma bin_to_bl_aux_Bit_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (w BIT b) bl =
- bin_to_bl_aux (n - 1) w (b # bl)"
+ "0 < n \<Longrightarrow> bin_to_bl_aux n (w BIT b) bl = bin_to_bl_aux (n - 1) w (b # bl)"
by (cases n) auto
lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit0 w)) bl =
- bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
+ "0 < n \<Longrightarrow>
+ bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
by (cases n) auto
lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl =
- bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
+ "0 < n \<Longrightarrow>
+ bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
by (cases n) auto
text \<open>Link between bin and bool list.\<close>
-lemma bl_to_bin_aux_append:
- "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
+lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
by (induct bs arbitrary: w) auto
-lemma bin_to_bl_aux_append:
- "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
+lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
by (induct n arbitrary: w bs) auto
-lemma bl_to_bin_append:
- "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
+lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
-lemma bin_to_bl_aux_alt:
- "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
- unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
+lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
+ by (simp add: bin_to_bl_def bin_to_bl_aux_append)
lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
- unfolding bin_to_bl_def by auto
+ by (auto simp: bin_to_bl_def)
-lemma size_bin_to_bl_aux:
- "size (bin_to_bl_aux n w bs) = n + length bs"
+lemma size_bin_to_bl_aux: "size (bin_to_bl_aux n w bs) = n + length bs"
by (induct n arbitrary: w bs) auto
-lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n"
- unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
+lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n"
+ by (simp add: bin_to_bl_def size_bin_to_bl_aux)
-lemma bin_bl_bin':
- "bl_to_bin (bin_to_bl_aux n w bs) =
- bl_to_bin_aux bs (bintrunc n w)"
- by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
+lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
+ by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def)
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
- unfolding bin_to_bl_def bin_bl_bin' by auto
+ by (auto simp: bin_to_bl_def bin_bl_bin')
-lemma bl_bin_bl':
- "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) =
- bin_to_bl_aux n w bs"
+lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
apply (induct bs arbitrary: w n)
apply auto
- apply (simp_all only : add_Suc [symmetric])
- apply (auto simp add : bin_to_bl_def)
+ apply (simp_all only: add_Suc [symmetric])
+ apply (auto simp add: bin_to_bl_def)
done
lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
@@ -182,9 +161,8 @@
apply (rule bin_to_bl_aux.Z)
apply simp
done
-
-lemma bl_to_bin_inj:
- "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
+
+lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
apply (rule_tac box_equals)
defer
apply (rule bl_bin_bl)
@@ -193,86 +171,74 @@
done
lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
- unfolding bl_to_bin_def by auto
+ by (auto simp: bl_to_bin_def)
lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
- unfolding bl_to_bin_def by auto
+ by (auto simp: bl_to_bin_def)
-lemma bin_to_bl_zero_aux:
- "bin_to_bl_aux n 0 bl = replicate n False @ bl"
+lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
- unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
+ by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
-lemma bin_to_bl_minus1_aux:
- "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
+lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
- unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
+ by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
-lemma bl_to_bin_rep_F:
- "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
- apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
- apply (simp add: bl_to_bin_def)
- done
+lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
+ by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
-lemma bin_to_bl_trunc [simp]:
- "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
+lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
by (auto intro: bl_to_bin_inj)
lemma bin_to_bl_aux_bintr:
- "bin_to_bl_aux n (bintrunc m bin) bl =
+ "bin_to_bl_aux n (bintrunc m bin) bl =
replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
apply (induct n arbitrary: m bin bl)
apply clarsimp
apply clarsimp
apply (case_tac "m")
- apply (clarsimp simp: bin_to_bl_zero_aux)
+ apply (clarsimp simp: bin_to_bl_zero_aux)
apply (erule thin_rl)
- apply (induct_tac n)
+ apply (induct_tac n)
apply auto
done
lemma bin_to_bl_bintr:
- "bin_to_bl n (bintrunc m bin) =
- replicate (n - m) False @ bin_to_bl (min n m) bin"
+ "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
by (induct n) auto
-lemma len_bin_to_bl_aux:
- "length (bin_to_bl_aux n w bs) = n + length bs"
+lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
by (fact size_bin_to_bl_aux)
-lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
+lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
by (fact size_bin_to_bl) (* FIXME: duplicate *)
-
-lemma sign_bl_bin':
- "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
+
+lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
by (induct bs arbitrary: w) auto
-
+
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
- unfolding bl_to_bin_def by (simp add : sign_bl_bin')
-
-lemma bl_sbin_sign_aux:
- "hd (bin_to_bl_aux (Suc n) w bs) =
- (bin_sign (sbintrunc n w) = -1)"
+ by (simp add: bl_to_bin_def sign_bl_bin')
+
+lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
apply (induct n arbitrary: w bs)
apply clarsimp
apply (cases w rule: bin_exhaust)
apply simp
done
-
-lemma bl_sbin_sign:
- "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
+
+lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
lemma bin_nth_of_bl_aux:
- "bin_nth (bl_to_bin_aux bl w) n =
- (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
+ "bin_nth (bl_to_bin_aux bl w) n =
+ (n < size bl \<and> rev bl ! n | n \<ge> length bl \<and> bin_nth w (n - size bl))"
apply (induct bl arbitrary: w)
apply clarsimp
apply clarsimp
@@ -281,8 +247,8 @@
apply auto
done
-lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
- unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
+lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
+ by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
apply (induct n arbitrary: m w)
@@ -296,11 +262,10 @@
apply (simp add: bin_to_bl_aux_alt)
done
-lemma nth_rev:
- "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
+lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
apply (induct xs)
apply simp
- apply (clarsimp simp add : nth_append nth.simps split: nat.split)
+ apply (clarsimp simp add: nth_append nth.simps split: nat.split)
apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
apply arith
done
@@ -309,7 +274,7 @@
by (simp add: nth_rev)
lemma nth_bin_to_bl_aux:
- "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
+ "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
(if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
apply (induct m arbitrary: w n bl)
apply clarsimp
@@ -318,29 +283,29 @@
apply simp
done
-lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
- unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
+lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
+ by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
-lemma bl_to_bin_lt2p_aux:
- "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
apply (induct bs arbitrary: w)
apply clarsimp
apply clarsimp
apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+
done
-lemma bl_to_bin_lt2p_drop:
- "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
+lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
proof (induct bs)
+ case Nil
+ then show ?case by simp
+next
case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
show ?case unfolding bl_to_bin_def by simp
-qed simp
+qed
lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
-lemma bl_to_bin_ge2p_aux:
- "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
+lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
apply (induct bs arbitrary: w)
apply clarsimp
apply clarsimp
@@ -349,15 +314,14 @@
apply (simp add: Bit_def)
done
-lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
+lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
apply (unfold bl_to_bin_def)
apply (rule xtrans(4))
apply (rule bl_to_bin_ge2p_aux)
apply simp
done
-lemma butlast_rest_bin:
- "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
+lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
apply (unfold bin_to_bl_def)
apply (cases w rule: bin_exhaust)
apply (cases n, clarsimp)
@@ -365,180 +329,154 @@
apply (auto simp add: bin_to_bl_aux_alt)
done
-lemma butlast_bin_rest:
- "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
+lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
lemma butlast_rest_bl2bin_aux:
- "bl ~= [] \<Longrightarrow>
- bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
+ "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
by (induct bl arbitrary: w) auto
-
-lemma butlast_rest_bl2bin:
- "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
- apply (unfold bl_to_bin_def)
- apply (cases bl)
- apply (auto simp add: butlast_rest_bl2bin_aux)
- done
+
+lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
+ by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
lemma trunc_bl2bin_aux:
- "bintrunc m (bl_to_bin_aux bl w) =
+ "bintrunc m (bl_to_bin_aux bl w) =
bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
proof (induct bl arbitrary: w)
- case Nil show ?case by simp
+ case Nil
+ show ?case by simp
next
- case (Cons b bl) show ?case
+ case (Cons b bl)
+ show ?case
proof (cases "m - length bl")
- case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp
+ case 0
+ then have "Suc (length bl) - m = Suc (length bl - m)" by simp
with Cons show ?thesis by simp
next
- case (Suc n) then have *: "m - Suc (length bl) = n" by simp
- with Suc Cons show ?thesis by simp
+ case (Suc n)
+ then have "m - Suc (length bl) = n" by simp
+ with Cons Suc show ?thesis by simp
qed
qed
-lemma trunc_bl2bin:
- "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
- unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
-
-lemma trunc_bl2bin_len [simp]:
- "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
+lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
+ by (simp add: bl_to_bin_def trunc_bl2bin_aux)
+
+lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
by (simp add: trunc_bl2bin)
-lemma bl2bin_drop:
- "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
+lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
apply (rule trans)
prefer 2
apply (rule trunc_bl2bin [symmetric])
- apply (cases "k <= length bl")
+ apply (cases "k \<le> length bl")
apply auto
done
-lemma nth_rest_power_bin:
- "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
- apply (induct k arbitrary: n, clarsimp)
+lemma nth_rest_power_bin: "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
+ apply (induct k arbitrary: n)
+ apply clarsimp
apply clarsimp
apply (simp only: bin_nth.Suc [symmetric] add_Suc)
done
-lemma take_rest_power_bin:
- "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
+lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
done
-lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
+lemma hd_butlast: "size xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
by (cases xs) auto
-lemma last_bin_last':
- "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
+lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
by (induct xs arbitrary: w) auto
-lemma last_bin_last:
- "size xs > 0 ==> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
+lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
unfolding bl_to_bin_def by (erule last_bin_last')
-
-lemma bin_last_last:
- "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
- apply (unfold bin_to_bl_def)
- apply simp
- apply (auto simp add: bin_to_bl_aux_alt)
- done
+
+lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
+ by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
+
-(** links between bit-wise operations and operations on bool lists **)
-
+subsection \<open>Links between bit-wise operations and operations on bool lists\<close>
+
lemma bl_xor_aux_bin:
- "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
+ "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
apply (induct n arbitrary: v w bs cs)
apply simp
apply (case_tac v rule: bin_exhaust)
apply (case_tac w rule: bin_exhaust)
apply clarsimp
apply (case_tac b)
- apply auto
+ apply auto
done
lemma bl_or_aux_bin:
- "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
+ "map2 (op \<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v OR w) (map2 (op \<or>) bs cs)"
apply (induct n arbitrary: v w bs cs)
apply simp
apply (case_tac v rule: bin_exhaust)
apply (case_tac w rule: bin_exhaust)
apply clarsimp
done
-
+
lemma bl_and_aux_bin:
- "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)"
+ "map2 (op \<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v AND w) (map2 (op \<and>) bs cs)"
apply (induct n arbitrary: v w bs cs)
apply simp
apply (case_tac v rule: bin_exhaust)
apply (case_tac w rule: bin_exhaust)
apply clarsimp
done
-
-lemma bl_not_aux_bin:
- "map Not (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (NOT w) (map Not cs)"
- apply (induct n arbitrary: w cs)
- apply clarsimp
- apply clarsimp
- done
+
+lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
+ by (induct n arbitrary: w cs) auto
lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
- unfolding bin_to_bl_def by (simp add: bl_not_aux_bin)
+ by (simp add: bin_to_bl_def bl_not_aux_bin)
-lemma bl_and_bin:
- "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
- unfolding bin_to_bl_def by (simp add: bl_and_aux_bin)
+lemma bl_and_bin: "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
+ by (simp add: bin_to_bl_def bl_and_aux_bin)
-lemma bl_or_bin:
- "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
- unfolding bin_to_bl_def by (simp add: bl_or_aux_bin)
+lemma bl_or_bin: "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
+ by (simp add: bin_to_bl_def bl_or_aux_bin)
-lemma bl_xor_bin:
- "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
- unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil)
+lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+ by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
lemma drop_bin2bl_aux:
- "drop m (bin_to_bl_aux n bin bs) =
+ "drop m (bin_to_bl_aux n bin bs) =
bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
apply (induct n arbitrary: m bin bs, clarsimp)
apply clarsimp
apply (case_tac bin rule: bin_exhaust)
- apply (case_tac "m <= n", simp)
+ apply (case_tac "m \<le> n", simp)
apply (case_tac "m - n", simp)
apply simp
- apply (rule_tac f = "%nat. drop nat bs" in arg_cong)
+ apply (rule_tac f = "\<lambda>nat. drop nat bs" in arg_cong)
apply simp
done
lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
- unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux)
+ by (simp add: bin_to_bl_def drop_bin2bl_aux)
-lemma take_bin2bl_lem1:
- "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
- apply (induct m arbitrary: w bs, clarsimp)
+lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
+ apply (induct m arbitrary: w bs)
+ apply clarsimp
apply clarsimp
apply (simp add: bin_to_bl_aux_alt)
apply (simp add: bin_to_bl_def)
apply (simp add: bin_to_bl_aux_alt)
done
-lemma take_bin2bl_lem:
- "take m (bin_to_bl_aux (m + n) w bs) =
- take m (bin_to_bl (m + n) w)"
- apply (induct n arbitrary: w bs)
- apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1)
- apply simp
- done
+lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
+ by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
-lemma bin_split_take:
- "bin_split n c = (a, b) \<Longrightarrow>
- bin_to_bl m a = take m (bin_to_bl (m + n) c)"
+lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
apply (induct n arbitrary: b c)
apply clarsimp
apply (clarsimp simp: Let_def split: prod.split_asm)
@@ -546,71 +484,59 @@
apply (simp add: take_bin2bl_lem)
done
-lemma bin_split_take1:
- "k = m + n ==> bin_split n c = (a, b) ==>
- bin_to_bl m a = take m (bin_to_bl k c)"
+lemma bin_split_take1:
+ "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
by (auto elim: bin_split_take)
-
-lemma nth_takefill: "m < n \<Longrightarrow>
- takefill fill n l ! m = (if m < length l then l ! m else fill)"
- apply (induct n arbitrary: m l, clarsimp)
+
+lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
+ apply (induct n arbitrary: m l)
+ apply clarsimp
apply clarsimp
apply (case_tac m)
apply (simp split: list.split)
apply (simp split: list.split)
done
-lemma takefill_alt:
- "takefill fill n l = take n l @ replicate (n - length l) fill"
+lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
by (induct n arbitrary: l) (auto split: list.split)
-lemma takefill_replicate [simp]:
- "takefill fill n (replicate m fill) = replicate n fill"
- by (simp add : takefill_alt replicate_add [symmetric])
+lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
+ by (simp add: takefill_alt replicate_add [symmetric])
-lemma takefill_le':
- "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
by (induct m arbitrary: l n) (auto split: list.split)
lemma length_takefill [simp]: "length (takefill fill n l) = n"
- by (simp add : takefill_alt)
+ by (simp add: takefill_alt)
-lemma take_takefill':
- "!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w"
- by (induct k) (auto split: list.split)
+lemma take_takefill': "\<And>w n. n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
+ by (induct k) (auto split: list.split)
-lemma drop_takefill:
- "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
- by (induct k) (auto split: list.split)
+lemma drop_takefill: "\<And>w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
+ by (induct k) (auto split: list.split)
-lemma takefill_le [simp]:
- "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
by (auto simp: le_iff_add takefill_le')
-lemma take_takefill [simp]:
- "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
+lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
by (auto simp: le_iff_add take_takefill')
-
-lemma takefill_append:
- "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
+
+lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
by (induct xs) auto
-lemma takefill_same':
- "l = length xs ==> takefill fill l xs = xs"
- by (induct xs arbitrary: l, auto)
-
+lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
+ by (induct xs arbitrary: l) auto
+
lemmas takefill_same [simp] = takefill_same' [OF refl]
-lemma takefill_bintrunc:
- "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
+lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
done
-lemma bl_bin_bl_rtf:
- "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
- by (simp add : takefill_bintrunc)
+lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
+ by (simp add: takefill_bintrunc)
lemma bl_bin_bl_rep_drop:
"bin_to_bl n (bl_to_bin bl) =
@@ -618,25 +544,24 @@
by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
lemma tf_rev:
- "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) =
+ "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
rev (takefill y m (rev (takefill x k (rev bl))))"
apply (rule nth_equalityI)
apply (auto simp add: nth_takefill nth_rev)
- apply (rule_tac f = "%n. bl ! n" in arg_cong)
- apply arith
+ apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
+ apply arith
done
-lemma takefill_minus:
- "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
+lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
by auto
-lemmas takefill_Suc_cases =
+lemmas takefill_Suc_cases =
list.cases [THEN takefill.Suc [THEN trans]]
lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
-lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
+lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
takefill_minus [symmetric, THEN trans]]
lemma takefill_numeral_Nil [simp]:
@@ -647,32 +572,29 @@
"takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
by (simp add: numeral_eq_Suc)
-(* links with function bl_to_bin *)
+
+subsection \<open>Links with function \<open>bl_to_bin\<close>\<close>
-lemma bl_to_bin_aux_cat:
- "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) =
+lemma bl_to_bin_aux_cat:
+ "\<And>nv v. bl_to_bin_aux bs (bin_cat w nv v) =
bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
- apply (induct bs)
- apply simp
- apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
- done
+ by (induct bs) (simp, simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
-lemma bin_to_bl_aux_cat:
- "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
+lemma bin_to_bl_aux_cat:
+ "\<And>w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
- by (induct nw) auto
+ by (induct nw) auto
-lemma bl_to_bin_aux_alt:
- "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
+lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
- unfolding bl_to_bin_def [symmetric] by simp
+ by (simp add: bl_to_bin_def [symmetric])
lemma bin_to_bl_cat:
"bin_to_bl (nv + nw) (bin_cat v nw w) =
bin_to_bl_aux nv v (bin_to_bl nw w)"
- unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat)
+ by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
-lemmas bl_to_bin_aux_app_cat =
+lemmas bl_to_bin_aux_app_cat =
trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
lemmas bin_to_bl_aux_cat_app =
@@ -686,49 +608,46 @@
"bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
-(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
-lemma bl_to_bin_app_cat_alt:
- "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
- by (simp add : bl_to_bin_app_cat)
+text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
+lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
+ by (simp add: bl_to_bin_app_cat)
-lemma mask_lem: "(bl_to_bin (True # replicate n False)) =
- (bl_to_bin (replicate n True)) + 1"
+lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
apply (unfold bl_to_bin_def)
apply (induct n)
apply simp
- apply (simp only: Suc_eq_plus1 replicate_add
- append_Cons [symmetric] bl_to_bin_aux_append)
+ apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
apply (simp add: Bit_B0_2t Bit_B1_2t)
done
-(* function bl_of_nth *)
+
+subsection \<open>Function \<open>bl_of_nth\<close>\<close>
+
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
by (induct n) auto
-lemma nth_bl_of_nth [simp]:
- "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
+lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
apply (induct n)
apply simp
- apply (clarsimp simp add : nth_append)
- apply (rule_tac f = "f" in arg_cong)
+ apply (clarsimp simp add: nth_append)
+ apply (rule_tac f = "f" in arg_cong)
apply simp
done
-lemma bl_of_nth_inj:
- "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
+lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
by (induct n) auto
-lemma bl_of_nth_nth_le:
- "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
- apply (induct n arbitrary: xs, clarsimp)
+lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
+ apply (induct n arbitrary: xs)
+ apply clarsimp
apply clarsimp
apply (rule trans [OF _ hd_Cons_tl])
apply (frule Suc_le_lessD)
apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
apply (subst hd_drop_conv_nth)
- apply force
- apply simp_all
- apply (rule_tac f = "%n. drop n xs" in arg_cong)
+ apply force
+ apply simp_all
+ apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
apply simp
done
@@ -741,45 +660,44 @@
lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
by (induct bl) auto
-lemma size_rbl_add:
- "!!cl. length (rbl_add bl cl) = length bl"
- by (induct bl) (auto simp: Let_def size_rbl_succ)
+lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
+ by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
-lemma size_rbl_mult:
- "!!cl. length (rbl_mult bl cl) = length bl"
- by (induct bl) (auto simp add : Let_def size_rbl_add)
+lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
+ by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
-lemmas rbl_sizes [simp] =
+lemmas rbl_sizes [simp] =
size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
lemmas rbl_Nils =
rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
-lemma rbl_pred:
- "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
- apply (induct n arbitrary: bin, simp)
+lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
apply (unfold bin_to_bl_def)
+ apply (induct n arbitrary: bin)
+ apply simp
apply clarsimp
apply (case_tac bin rule: bin_exhaust)
apply (case_tac b)
apply (clarsimp simp: bin_to_bl_aux_alt)+
done
-lemma rbl_succ:
- "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
- apply (induct n arbitrary: bin, simp)
+lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
apply (unfold bin_to_bl_def)
+ apply (induct n arbitrary: bin)
+ apply simp
apply clarsimp
apply (case_tac bin rule: bin_exhaust)
apply (case_tac b)
apply (clarsimp simp: bin_to_bl_aux_alt)+
done
-lemma rbl_add:
- "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+lemma rbl_add:
+ "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
rev (bin_to_bl n (bina + binb))"
- apply (induct n, simp)
apply (unfold bin_to_bl_def)
+ apply (induct n)
+ apply simp
apply clarsimp
apply (case_tac bina rule: bin_exhaust)
apply (case_tac binb rule: bin_exhaust)
@@ -788,82 +706,77 @@
apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
done
-lemma rbl_add_app2:
- "!!blb. length blb >= length bla ==>
- rbl_add bla (blb @ blc) = rbl_add bla blb"
- apply (induct bla, simp)
+lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
+ apply (induct bla arbitrary: blb)
+ apply simp
apply clarsimp
apply (case_tac blb, clarsimp)
apply (clarsimp simp: Let_def)
done
-lemma rbl_add_take2:
- "!!blb. length blb >= length bla ==>
- rbl_add bla (take (length bla) blb) = rbl_add bla blb"
- apply (induct bla, simp)
+lemma rbl_add_take2:
+ "length blb >= length bla ==> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
+ apply (induct bla arbitrary: blb)
+ apply simp
apply clarsimp
apply (case_tac blb, clarsimp)
apply (clarsimp simp: Let_def)
done
-lemma rbl_add_long:
- "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+lemma rbl_add_long:
+ "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
rev (bin_to_bl n (bina + binb))"
apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
- apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
+ apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
apply (rule rev_swap [THEN iffD1])
apply (simp add: rev_take drop_bin2bl)
apply simp
done
-lemma rbl_mult_app2:
- "!!blb. length blb >= length bla ==>
- rbl_mult bla (blb @ blc) = rbl_mult bla blb"
- apply (induct bla, simp)
+lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
+ apply (induct bla arbitrary: blb)
+ apply simp
apply clarsimp
apply (case_tac blb, clarsimp)
apply (clarsimp simp: Let_def rbl_add_app2)
done
-lemma rbl_mult_take2:
- "length blb >= length bla ==>
- rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
+lemma rbl_mult_take2:
+ "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
apply (rule trans)
apply (rule rbl_mult_app2 [symmetric])
apply simp
- apply (rule_tac f = "rbl_mult bla" in arg_cong)
+ apply (rule_tac f = "rbl_mult bla" in arg_cong)
apply (rule append_take_drop_id)
done
-
-lemma rbl_mult_gt1:
- "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) =
+
+lemma rbl_mult_gt1:
+ "m \<ge> length bl \<Longrightarrow>
+ rbl_mult bl (rev (bin_to_bl m binb)) =
rbl_mult bl (rev (bin_to_bl (length bl) binb))"
apply (rule trans)
apply (rule rbl_mult_take2 [symmetric])
apply simp_all
- apply (rule_tac f = "rbl_mult bl" in arg_cong)
+ apply (rule_tac f = "rbl_mult bl" in arg_cong)
apply (rule rev_swap [THEN iffD1])
apply (simp add: rev_take drop_bin2bl)
done
-
-lemma rbl_mult_gt:
- "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+
+lemma rbl_mult_gt:
+ "m > n \<Longrightarrow>
+ rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
by (auto intro: trans [OF rbl_mult_gt1])
-
+
lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
-lemma rbbl_Cons:
- "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
- apply (unfold bin_to_bl_def)
- apply simp
- apply (simp add: bin_to_bl_aux_alt)
- done
+lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
+ by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
-lemma rbl_mult: "!!bina binb.
- rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+lemma rbl_mult:
+ "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
rev (bin_to_bl n (bina * binb))"
- apply (induct n)
+ apply (induct n arbitrary: bina binb)
apply simp
apply (unfold bin_to_bl_def)
apply clarsimp
@@ -875,32 +788,28 @@
apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
done
-lemma rbl_add_split:
- "P (rbl_add (y # ys) (x # xs)) =
- (ALL ws. length ws = length ys --> ws = rbl_add ys xs -->
- (y --> ((x --> P (False # rbl_succ ws)) & (~ x --> P (True # ws)))) &
- (~ y --> P (x # ws)))"
- apply (auto simp add: Let_def)
- apply (case_tac [!] "y")
- apply auto
- done
+lemma rbl_add_split:
+ "P (rbl_add (y # ys) (x # xs)) =
+ (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
+ (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
+ (\<not> y \<longrightarrow> P (x # ws)))"
+ by (cases y) (auto simp: Let_def)
-lemma rbl_mult_split:
- "P (rbl_mult (y # ys) xs) =
- (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs -->
- (y --> P (rbl_add ws xs)) & (~ y --> P ws))"
- by (clarsimp simp add : Let_def)
-
+lemma rbl_mult_split:
+ "P (rbl_mult (y # ys) xs) =
+ (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
+ (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
+ by (auto simp: Let_def)
-subsection "Repeated splitting or concatenation"
-lemma sclem:
- "size (concat (map (bin_to_bl n) xs)) = length xs * n"
+subsection \<open>Repeated splitting or concatenation\<close>
+
+lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
by (induct xs) auto
lemma bin_cat_foldl_lem:
- "foldl (%u. bin_cat u n) x xs =
- bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
+ "foldl (\<lambda>u. bin_cat u n) x xs =
+ bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
apply (induct xs arbitrary: x)
apply simp
apply (simp (no_asm))
@@ -908,17 +817,16 @@
apply (drule meta_spec)
apply (erule trans)
apply (drule_tac x = "bin_cat y n a" in meta_spec)
- apply (simp add : bin_cat_assoc_sym min.absorb2)
+ apply (simp add: bin_cat_assoc_sym min.absorb2)
done
-lemma bin_rcat_bl:
- "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
+lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
apply (unfold bin_rcat_def)
apply (rule sym)
apply (induct wl)
- apply (auto simp add : bl_to_bin_append)
- apply (simp add : bl_to_bin_aux_alt sclem)
- apply (simp add : bin_cat_foldl_lem [symmetric])
+ apply (auto simp add: bl_to_bin_append)
+ apply (simp add: bl_to_bin_aux_alt sclem)
+ apply (simp add: bin_cat_foldl_lem [symmetric])
done
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
@@ -934,19 +842,17 @@
lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
lemmas rbscl = bin_rsplit_aux_simp2s (2)
-lemmas rsplit_aux_0_simps [simp] =
+lemmas rsplit_aux_0_simps [simp] =
rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
-lemma bin_rsplit_aux_append:
- "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
+lemma bin_rsplit_aux_append: "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
apply (induct n m c bs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp split: prod.split)
done
-lemma bin_rsplitl_aux_append:
- "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
+lemma bin_rsplitl_aux_append: "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
apply (induct n m c bs rule: bin_rsplitl_aux.induct)
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplitl_aux.simps)
@@ -958,41 +864,38 @@
lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
-lemmas rsplit_aux_alts = rsplit_aux_apps
+lemmas rsplit_aux_alts = rsplit_aux_apps
[unfolded append_Nil rsplit_def_auxs [symmetric]]
-lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
+lemma bin_split_minus: "0 < n \<Longrightarrow> bin_split (Suc (n - 1)) w = bin_split n w"
by auto
lemmas bin_split_minus_simp =
bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]]
-lemma bin_split_pred_simp [simp]:
+lemma bin_split_pred_simp [simp]:
"(0::nat) < numeral bin \<Longrightarrow>
- bin_split (numeral bin) w =
- (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w)
- in (w1, w2 BIT bin_last w))"
+ bin_split (numeral bin) w =
+ (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w)
+ in (w1, w2 BIT bin_last w))"
by (simp only: bin_split_minus_simp)
lemma bin_rsplit_aux_simp_alt:
"bin_rsplit_aux n m c bs =
- (if m = 0 \<or> n = 0
- then bs
- else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
- unfolding bin_rsplit_aux.simps [of n m c bs]
- apply simp
+ (if m = 0 \<or> n = 0 then bs
+ else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
+ apply (simp add: bin_rsplit_aux.simps [of n m c bs])
apply (subst rsplit_aux_alts)
apply (simp add: bin_rsplit_def)
done
-lemmas bin_rsplit_simp_alt =
+lemmas bin_rsplit_simp_alt =
trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
-lemma bin_rsplit_size_sign' [rule_format] :
- "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow>
- (ALL v: set sw. bintrunc n v = v)"
+lemma bin_rsplit_size_sign' [rule_format]:
+ "n > 0 \<Longrightarrow> rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. bintrunc n v = v"
apply (induct sw arbitrary: nw w)
apply clarsimp
apply clarsimp
@@ -1003,12 +906,14 @@
apply simp
done
-lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
+lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
lemma bin_nth_rsplit [rule_format] :
- "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) -->
- k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
+ "n > 0 \<Longrightarrow> m < n \<Longrightarrow>
+ \<forall>w k nw.
+ rev sw = bin_rsplit n (nw, w) \<longrightarrow>
+ k < size sw \<longrightarrow> bin_nth (sw ! k) m = bin_nth w (k * n + m)"
apply (induct sw)
apply clarsimp
apply clarsimp
@@ -1017,24 +922,21 @@
apply clarify
apply (erule allE, erule impE, erule exI)
apply (case_tac k)
- apply clarsimp
+ apply clarsimp
prefer 2
apply clarsimp
apply (erule allE)
apply (erule (1) impE)
- apply (drule bin_nth_split, erule conjE, erule allE,
- erule trans, simp add : ac_simps)+
+ apply (drule bin_nth_split, erule conjE, erule allE, erule trans, simp add: ac_simps)+
done
-lemma bin_rsplit_all:
- "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
- unfolding bin_rsplit_def
- by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: prod.split)
+lemma bin_rsplit_all: "0 < nw \<Longrightarrow> nw \<le> n \<Longrightarrow> bin_rsplit n (nw, w) = [bintrunc n w]"
+ by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc)
-lemma bin_rsplit_l [rule_format] :
- "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
+lemma bin_rsplit_l [rule_format]:
+ "\<forall>bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
- apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
+ apply (simp (no_asm) add: bin_rsplitl_def bin_rsplit_def)
apply (rule allI)
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplit_aux.simps)
@@ -1048,10 +950,10 @@
apply simp
done
-lemma bin_rsplit_rcat [rule_format] :
- "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
+lemma bin_rsplit_rcat [rule_format]:
+ "n > 0 \<longrightarrow> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
apply (unfold bin_rsplit_def bin_rcat_def)
- apply (rule_tac xs = "ws" in rev_induct)
+ apply (rule_tac xs = ws in rev_induct)
apply clarsimp
apply clarsimp
apply (subst rsplit_aux_alts)
@@ -1063,78 +965,75 @@
"\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
proof -
- { fix i j j' k k' m :: nat and R
- assume d: "(i::nat) \<le> j \<or> m < j'"
- assume R1: "i * k \<le> j * k \<Longrightarrow> R"
- assume R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
- have "R" using d
- apply safe
- apply (rule R1, erule mult_le_mono1)
- apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
- done
- } note A = this
- { fix sc m n lb :: nat
- have "(0::nat) < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
- apply safe
- apply arith
- apply (case_tac "sc >= n")
- apply arith
- apply (insert linorder_le_less_linear [of m lb])
- apply (erule_tac k2=n and k'2=n in A)
- apply arith
- apply simp
- done
- } note B = this
+ have *: R
+ if d: "i \<le> j \<or> m < j'"
+ and R1: "i * k \<le> j * k \<Longrightarrow> R"
+ and R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
+ for i j j' k k' m :: nat and R
+ using d
+ apply safe
+ apply (rule R1, erule mult_le_mono1)
+ apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
+ done
+ have **: "0 < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
+ for sc m n lb :: nat
+ apply safe
+ apply arith
+ apply (case_tac "sc \<ge> n")
+ apply arith
+ apply (insert linorder_le_less_linear [of m lb])
+ apply (erule_tac k=n and k'=n in *)
+ apply arith
+ apply simp
+ done
show ?thesis
apply (induct n nw w bs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
- apply (simp add: B Let_def split: prod.split)
+ apply (simp add: ** Let_def split: prod.split)
done
qed
-lemma bin_rsplit_len_le:
- "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
- unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
-
+lemma bin_rsplit_len_le: "n \<noteq> 0 \<longrightarrow> ws = bin_rsplit n (nw, w) \<longrightarrow> length ws \<le> m \<longleftrightarrow> nw \<le> m * n"
+ by (auto simp: bin_rsplit_def bin_rsplit_aux_len_le)
+
lemma bin_rsplit_aux_len:
- "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) =
- (nw + n - 1) div n + length cs"
+ "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs"
apply (induct n nw w cs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp simp: Let_def split: prod.split)
apply (erule thin_rl)
apply (case_tac m)
- apply simp
- apply (case_tac "m <= n")
+ apply simp
+ apply (case_tac "m \<le> n")
apply (auto simp add: div_add_self2)
done
-lemma bin_rsplit_len:
- "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
- unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
+lemma bin_rsplit_len: "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
+ by (auto simp: bin_rsplit_def bin_rsplit_aux_len)
lemma bin_rsplit_aux_len_indep:
"n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
length (bin_rsplit_aux n nw v bs) =
length (bin_rsplit_aux n nw w cs)"
proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
- case (1 n m w cs v bs) show ?case
+ case (1 n m w cs v bs)
+ show ?case
proof (cases "m = 0")
- case True then show ?thesis using \<open>length bs = length cs\<close> by simp
+ case True
+ with \<open>length bs = length cs\<close> show ?thesis by simp
next
case False
from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
length (bin_rsplit_aux n (m - n) v bs) =
length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
- by auto
- show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close>
- by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
- split: prod.split)
+ by auto
+ from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis
+ by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split)
qed
qed
-lemma bin_rsplit_len_indep:
- "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
+lemma bin_rsplit_len_indep:
+ "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
apply (unfold bin_rsplit_def)
apply (simp (no_asm))
apply (erule bin_rsplit_aux_len_indep)
@@ -1147,33 +1046,27 @@
instantiation int :: bitss
begin
-definition [iff]:
- "i !! n \<longleftrightarrow> bin_nth i n"
+definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
-definition
- "lsb i = (i :: int) !! 0"
+definition "lsb i = i !! 0" for i :: int
-definition
- "set_bit i n b = bin_sc n b i"
+definition "set_bit i n b = bin_sc n b i"
definition
"set_bits f =
- (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
- let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
- in bl_to_bin (rev (map f [0..<n]))
- else if \<exists>n. \<forall>n'\<ge>n. f n' then
- let n = LEAST n. \<forall>n'\<ge>n. f n'
- in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
- else 0 :: int)"
+ (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+ let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+ in bl_to_bin (rev (map f [0..<n]))
+ else if \<exists>n. \<forall>n'\<ge>n. f n' then
+ let n = LEAST n. \<forall>n'\<ge>n. f n'
+ in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+ else 0 :: int)"
-definition
- "shiftl x n = (x :: int) * 2 ^ n"
+definition "shiftl x n = x * 2 ^ n" for x :: int
-definition
- "shiftr x n = (x :: int) div 2 ^ n"
+definition "shiftr x n = x div 2 ^ n" for x :: int
-definition
- "msb x \<longleftrightarrow> (x :: int) < 0"
+definition "msb x \<longleftrightarrow> x < 0" for x :: int
instance ..
--- a/src/HOL/Word/Examples/WordExamples.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,13 +1,13 @@
-(*
- Authors: Gerwin Klein and Thomas Sewell, NICTA
+(* Title: HOL/Word/Examples/WordExamples.thy
+ Authors: Gerwin Klein and Thomas Sewell, NICTA
- Examples demonstrating and testing various word operations.
+Examples demonstrating and testing various word operations.
*)
section "Examples of word operations"
theory WordExamples
-imports "../Word" "../WordBitwise"
+ imports "../Word" "../WordBitwise"
begin
type_synonym word32 = "32 word"
@@ -28,7 +28,7 @@
text "number ring simps"
-lemma
+lemma
"27 + 11 = (38::'a::len word)"
"27 + 11 = (6::5 word)"
"7 * 3 = (21::'a::len word)"
@@ -40,7 +40,7 @@
lemma "word_pred 2 = 1" by simp
lemma "word_succ (- 3) = -2" by simp
-
+
lemma "23 < (27::8 word)" by simp
lemma "23 \<le> (27::8 word)" by simp
lemma "\<not> 23 < (27::2 word)" by simp
@@ -69,8 +69,10 @@
lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
text "reducing goals to nat or int and arith:"
-lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
-lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+ by unat_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+ by unat_arith
text "bool lists"
@@ -111,7 +113,7 @@
lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
lemma "\<not> (1 :: 3 word) !! 2" by simp
-lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
+lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
@@ -133,7 +135,7 @@
lemma "\<not> msb (0::4 word)" by simp
lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
-lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
+lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
by simp
lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
@@ -171,20 +173,24 @@
text "more proofs using bitwise expansion"
-lemma "((x :: 10 word) AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+ for x :: "10 word"
by word_bitwise
-lemma "(((x :: 12 word) AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+ for x :: "12 word"
by word_bitwise
text "some problems require further reasoning after bit expansion"
-lemma "x \<le> (42 :: 8 word) \<Longrightarrow> x \<le> 89"
+lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
+ for x :: "8 word"
apply word_bitwise
apply blast
done
-lemma "((x :: word32) AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+ for x :: word32
apply word_bitwise
apply clarsimp
done
@@ -192,11 +198,10 @@
text "operations like shifts by non-numerals will expose some internal list
representations but may still be easy to solve"
-lemma shiftr_overflow:
- "32 \<le> a \<Longrightarrow> (b::word32) >> a = 0"
- apply (word_bitwise)
+lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
+ for b :: word32
+ apply word_bitwise
apply simp
done
-
end
--- a/src/HOL/Word/Misc_Numeric.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,76 +1,66 @@
-(*
- Author: Jeremy Dawson, NICTA
-*)
+(* Title: HOL/Word/Misc_Numeric.thy
+ Author: Jeremy Dawson, NICTA
+*)
section \<open>Useful Numerical Lemmas\<close>
theory Misc_Numeric
-imports Main
+ imports Main
begin
-lemma one_mod_exp_eq_one [simp]:
- "1 mod (2 * 2 ^ n) = (1::int)"
+lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)"
by (smt mod_pos_pos_trivial zero_less_power)
-lemma mod_2_neq_1_eq_eq_0:
- fixes k :: int
- shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
+lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
+ for k :: int
by (fact not_mod_2_eq_1_eq_0)
-lemma z1pmod2:
- fixes b :: int
- shows "(2 * b + 1) mod 2 = (1::int)"
+lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
+ for b :: int
by arith
-lemma diff_le_eq':
- "a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)"
+lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
+ for a b c :: int
by arith
-lemma emep1:
- fixes n d :: int
- shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+ for n d :: int
by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
-lemma int_mod_ge:
- "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
+lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
+ for a n :: int
by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
-lemma int_mod_ge':
- "b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n"
+lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
+ for b n :: int
by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
-lemma int_mod_le':
- "(0::int) \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+ for b n :: int
by (metis minus_mod_self2 zmod_le_nonneg_dividend)
-lemma zless2:
- "0 < (2 :: int)"
+lemma zless2: "0 < (2 :: int)"
by (fact zero_less_numeral)
-lemma zless2p:
- "0 < (2 ^ n :: int)"
+lemma zless2p: "0 < (2 ^ n :: int)"
by arith
-lemma zle2p:
- "0 \<le> (2 ^ n :: int)"
+lemma zle2p: "0 \<le> (2 ^ n :: int)"
by arith
-lemma m1mod2k:
- "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
+lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
using zless2p by (rule zmod_minus1)
-lemma p1mod22k':
- fixes b :: int
- shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
- using zle2p by (rule pos_zmod_mult_2)
+lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
+ for b :: int
+ using zle2p by (rule pos_zmod_mult_2)
-lemma p1mod22k:
- fixes b :: int
- shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
+lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
+ for b :: int
by (simp add: p1mod22k' add.commute)
-lemma int_mod_lem:
- "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
+lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
+ for b n :: int
apply safe
apply (erule (1) mod_pos_pos_trivial)
apply (erule_tac [!] subst)
@@ -78,4 +68,3 @@
done
end
-
--- a/src/HOL/Word/Misc_Typedef.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,4 +1,4 @@
-(*
+(*
Author: Jeremy Dawson and Gerwin Klein, NICTA
Consequences of type definition theorems, and of extended type definition.
@@ -18,7 +18,7 @@
tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
by (auto simp: type_definition_def)
-lemma td_nat_int:
+lemma td_nat_int:
"type_definition int nat (Collect (op <= 0))"
unfolding type_definition_def by auto
@@ -29,13 +29,13 @@
lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
by (simp add: Abs_inject)
-
-lemma Abs_inverse':
+
+lemma Abs_inverse':
"r : A ==> Abs r = a ==> Rep a = r"
by (safe elim!: Abs_inverse)
-lemma Rep_comp_inverse:
- "Rep o f = g ==> Abs o g = f"
+lemma Rep_comp_inverse:
+ "Rep \<circ> f = g ==> Abs \<circ> g = f"
using Rep_inverse by auto
lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
@@ -44,27 +44,27 @@
lemma Rep_inverse': "Rep a = r ==> Abs r = a"
by (safe intro!: Rep_inverse)
-lemma comp_Abs_inverse:
- "f o Abs = g ==> g o Rep = f"
+lemma comp_Abs_inverse:
+ "f \<circ> Abs = g ==> g \<circ> Rep = f"
using Rep_inverse by auto
-lemma set_Rep:
+lemma set_Rep:
"A = range Rep"
proof (rule set_eqI)
fix x
show "(x \<in> A) = (x \<in> range Rep)"
by (auto dest: Abs_inverse [of x, symmetric])
-qed
+qed
-lemma set_Rep_Abs: "A = range (Rep o Abs)"
+lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)"
proof (rule set_eqI)
fix x
- show "(x \<in> A) = (x \<in> range (Rep o Abs))"
+ show "(x \<in> A) = (x \<in> range (Rep \<circ> Abs))"
by (auto dest: Abs_inverse [of x, symmetric])
-qed
+qed
lemma Abs_inj_on: "inj_on Abs A"
- unfolding inj_on_def
+ unfolding inj_on_def
by (auto dest: Abs_inject [THEN iffD1])
lemma image: "Abs ` A = UNIV"
@@ -72,16 +72,16 @@
lemmas td_thm = type_definition_axioms
-lemma fns1:
- "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
+lemma fns1:
+ "Rep \<circ> fa = fr \<circ> Rep | fa \<circ> Abs = Abs \<circ> fr ==> Abs \<circ> fr \<circ> Rep = fa"
by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)
lemmas fns1a = disjI1 [THEN fns1]
lemmas fns1b = disjI2 [THEN fns1]
lemma fns4:
- "Rep o fa o Abs = fr ==>
- Rep o fa = fr o Rep & fa o Abs = Abs o fr"
+ "Rep \<circ> fa \<circ> Abs = fr ==>
+ Rep \<circ> fa = fr \<circ> Rep & fa \<circ> Abs = Abs \<circ> fr"
by auto
end
@@ -99,16 +99,16 @@
subsection "Extended form of type definition predicate"
lemma td_conds:
- "norm o norm = norm ==> (fr o norm = norm o fr) =
- (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
+ "norm \<circ> norm = norm ==> (fr \<circ> norm = norm \<circ> fr) =
+ (norm \<circ> fr \<circ> norm = fr \<circ> norm & norm \<circ> fr \<circ> norm = norm \<circ> fr)"
apply safe
apply (simp_all add: comp_assoc)
apply (simp_all add: o_assoc)
done
lemma fn_comm_power:
- "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n"
- apply (rule ext)
+ "fa \<circ> tr = tr \<circ> fr ==> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n"
+ apply (rule ext)
apply (induct n)
apply (auto dest: fun_cong)
done
@@ -122,15 +122,15 @@
assumes eq_norm: "\<And>x. Rep (Abs x) = norm x"
begin
-lemma Abs_norm [simp]:
+lemma Abs_norm [simp]:
"Abs (norm x) = Abs x"
using eq_norm [of x] by (auto elim: Rep_inverse')
lemma td_th:
- "g o Abs = f ==> f (Rep x) = g x"
+ "g \<circ> Abs = f ==> f (Rep x) = g x"
by (drule comp_Abs_inverse [symmetric]) simp
-lemma eq_norm': "Rep o Abs = norm"
+lemma eq_norm': "Rep \<circ> Abs = norm"
by (auto simp: eq_norm)
lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
@@ -141,42 +141,42 @@
lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w"
by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
-lemma inverse_norm:
+lemma inverse_norm:
"(Abs n = w) = (Rep w = norm n)"
apply (rule iffI)
apply (clarsimp simp add: eq_norm)
apply (simp add: eq_norm' [symmetric])
done
-lemma norm_eq_iff:
+lemma norm_eq_iff:
"(norm x = norm y) = (Abs x = Abs y)"
by (simp add: eq_norm' [symmetric])
-lemma norm_comps:
- "Abs o norm = Abs"
- "norm o Rep = Rep"
- "norm o norm = norm"
+lemma norm_comps:
+ "Abs \<circ> norm = Abs"
+ "norm \<circ> Rep = Rep"
+ "norm \<circ> norm = norm"
by (auto simp: eq_norm' [symmetric] o_def)
lemmas norm_norm [simp] = norm_comps
-lemma fns5:
- "Rep o fa o Abs = fr ==>
- fr o norm = fr & norm o fr = fr"
+lemma fns5:
+ "Rep \<circ> fa \<circ> Abs = fr ==>
+ fr \<circ> norm = fr & norm \<circ> fr = fr"
by (fold eq_norm') auto
(* following give conditions for converses to td_fns1
- the condition (norm o fr o norm = fr o norm) says that
+ the condition (norm \<circ> fr \<circ> norm = fr \<circ> norm) says that
fr takes normalised arguments to normalised results,
- (norm o fr o norm = norm o fr) says that fr
+ (norm \<circ> fr \<circ> norm = norm \<circ> fr) says that fr
takes norm-equivalent arguments to norm-equivalent results,
- (fr o norm = fr) says that fr
- takes norm-equivalent arguments to the same result, and
- (norm o fr = fr) says that fr takes any argument to a normalised result
+ (fr \<circ> norm = fr) says that fr
+ takes norm-equivalent arguments to the same result, and
+ (norm \<circ> fr = fr) says that fr takes any argument to a normalised result
*)
-lemma fns2:
- "Abs o fr o Rep = fa ==>
- (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)"
+lemma fns2:
+ "Abs \<circ> fr \<circ> Rep = fa ==>
+ (norm \<circ> fr \<circ> norm = fr \<circ> norm) = (Rep \<circ> fa = fr \<circ> Rep)"
apply (fold eq_norm')
apply safe
prefer 2
@@ -186,25 +186,25 @@
apply auto
done
-lemma fns3:
- "Abs o fr o Rep = fa ==>
- (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)"
+lemma fns3:
+ "Abs \<circ> fr \<circ> Rep = fa ==>
+ (norm \<circ> fr \<circ> norm = norm \<circ> fr) = (fa \<circ> Abs = Abs \<circ> fr)"
apply (fold eq_norm')
apply safe
prefer 2
apply (simp add: comp_assoc)
apply (rule ext)
- apply (drule_tac f="a o b" for a b in fun_cong)
+ apply (drule_tac f="a \<circ> b" for a b in fun_cong)
apply simp
done
-lemma fns:
- "fr o norm = norm o fr ==>
- (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)"
+lemma fns:
+ "fr \<circ> norm = norm \<circ> fr ==>
+ (fa \<circ> Abs = Abs \<circ> fr) = (Rep \<circ> fa = fr \<circ> Rep)"
apply safe
apply (frule fns1b)
- prefer 2
- apply (frule fns1a)
+ prefer 2
+ apply (frule fns1a)
apply (rule fns3 [THEN iffD1])
prefer 3
apply (rule fns2 [THEN iffD1])
@@ -213,7 +213,7 @@
done
lemma range_norm:
- "range (Rep o Abs) = A"
+ "range (Rep \<circ> Abs) = A"
by (simp add: set_Rep_Abs)
end
--- a/src/HOL/Word/Word.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Word.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1827,8 +1827,8 @@
by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
lemma unat_mult_lem:
- "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow>
- unat (x * y :: 'a::len word) = unat x * unat y"
+ "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
+ for x y :: "'a::len word"
by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
lemmas unat_plus_if' =
@@ -2002,7 +2002,7 @@
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
-lemma word_le_exists': "x \<le> y \<Longrightarrow> (\<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a))"
+lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a)"
for x y z :: "'a::len0 word"
apply (rule exI)
apply (rule conjI)
@@ -2330,13 +2330,15 @@
unfolding to_bl_def word_log_defs bl_and_bin
by (simp add: word_ubin.eq_norm)
-lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
+lemma word_lsb_alt: "lsb w = test_bit w 0"
+ for w :: "'a::len0 word"
by (auto simp: word_test_bit_def word_lsb_def)
lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
unfolding word_lsb_def uint_eq_0 uint_1 by simp
-lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
+lemma word_lsb_last: "lsb w = last (to_bl w)"
+ for w :: "'a::len word"
apply (unfold word_lsb_def uint_bl bin_to_bl_def)
apply (rule_tac bin="uint w" in bin_exhaust)
apply (cases "size w")
@@ -2419,7 +2421,7 @@
done
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
- unfolding of_bl_def bl_to_bin_rep_F by auto
+ by (auto simp: of_bl_def bl_to_bin_rep_F)
lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
for w :: "'a::len word"
@@ -2762,7 +2764,8 @@
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
by (simp add: of_bl_def bl_to_bin_append)
-lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
+lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
+ for w :: "'a::len0 word"
proof -
have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
by simp
@@ -2970,7 +2973,7 @@
for x :: "'a::len0 word"
using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
-lemma msb_shift: "msb w \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
+lemma msb_shift: "msb w \<longleftrightarrow> w >> (len_of TYPE('a) - 1) \<noteq> 0"
for w :: "'a::len word"
apply (unfold shiftr_bl word_msb_alt)
apply (simp add: word_size Suc_le_eq take_Suc)
@@ -3091,10 +3094,11 @@
apply auto
done
-lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
+lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
+ for b n :: int
by (simp add: int_mod_lem eq_sym_conv)
-lemma mask_eq_iff: "(w AND mask n) = w \<longleftrightarrow> uint w < 2 ^ n"
+lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
apply (simp add: and_mask_bintr)
apply (simp add: word_ubin.inverse_norm)
apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
@@ -3632,8 +3636,9 @@
split: prod.split)
lemma test_bit_rsplit:
- "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
- k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
+ "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
+ k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
+ for sw :: "'a::len word list"
apply (unfold word_rsplit_def word_test_bit_def)
apply (rule trans)
apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
@@ -3673,8 +3678,9 @@
done
lemma test_bit_rcat:
- "sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
+ "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
(n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
+ for wl :: "'a::len word list"
apply (unfold word_rcat_bl word_size)
apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
apply safe
@@ -4266,10 +4272,11 @@
by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
lemma unat_plus_if_size:
- "unat (x + (y::'a::len word)) =
+ "unat (x + y) =
(if unat x + unat y < 2^size x
then unat x + unat y
else unat x + unat y - 2^size x)"
+ for x y :: "'a::len word"
apply (subst word_arith_nat_defs)
apply (subst unat_of_nat)
apply (simp add: mod_nat_add word_size)
@@ -4339,7 +4346,7 @@
shows "(x - y) mod b = z' mod b'"
using assms [symmetric] by (auto intro: mod_diff_cong)
-lemma word_induct_less: "\<lbrakk>P 0; \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
for P :: "'a::len word \<Rightarrow> bool"
apply (cases m)
apply atomize
@@ -4362,11 +4369,11 @@
apply simp
done
-lemma word_induct: "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
for P :: "'a::len word \<Rightarrow> bool"
by (erule word_induct_less) simp
-lemma word_induct2 [induct type]: "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P n"
+lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
for P :: "'b::len word \<Rightarrow> bool"
apply (rule word_induct)
apply simp
@@ -4383,16 +4390,15 @@
lemma word_rec_0: "word_rec z s 0 = z"
by (simp add: word_rec_def)
-lemma word_rec_Suc:
- "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
+lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
+ for n :: "'a::len word"
apply (simp add: word_rec_def unat_word_ariths)
apply (subst nat_mod_eq')
apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
apply simp
done
-lemma word_rec_Pred:
- "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
+lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
apply (rule subst[where t="n" and s="1 + (n - 1)"])
apply simp
apply (subst word_rec_Suc)
@@ -4468,7 +4474,8 @@
apply simp
done
-lemma unatSuc: "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
+lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)"
+ for n :: "'a::len word"
by unat_arith
declare bin_to_bl_def [simp]
--- a/src/HOL/Word/WordBitwise.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/WordBitwise.thy Mon Apr 03 23:12:44 2017 +0200
@@ -2,24 +2,17 @@
Authors: Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
*)
-
theory WordBitwise
-
-imports Word
-
+ imports Word
begin
text \<open>Helper constants used in defining addition\<close>
-definition
- xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
-where
- "xor3 a b c = (a = (b = c))"
+definition xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
+ where "xor3 a b c = (a = (b = c))"
-definition
- carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
-where
- "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
+definition carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
+ where "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
lemma carry_simps:
"carry True a b = (a \<or> b)"
@@ -40,36 +33,28 @@
by (simp_all add: xor3_def)
text \<open>Breaking up word equalities into equalities on their
-bit lists. Equalities are generated and manipulated in the
-reverse order to to_bl.\<close>
+ bit lists. Equalities are generated and manipulated in the
+ reverse order to to_bl.\<close>
-lemma word_eq_rbl_eq:
- "(x = y) = (rev (to_bl x) = rev (to_bl y))"
+lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
by simp
-lemma rbl_word_or:
- "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def zip_rev bl_word_or rev_map)
-lemma rbl_word_and:
- "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def zip_rev bl_word_and rev_map)
-lemma rbl_word_xor:
- "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def zip_rev bl_word_xor rev_map)
-lemma rbl_word_not:
- "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
+lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
by (simp add: bl_word_not rev_map)
-lemma bl_word_sub:
- "to_bl (x - y) = to_bl (x + (- y))"
+lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
by simp
-lemma rbl_word_1:
- "rev (to_bl (1 :: ('a :: len0) word))
- = takefill False (len_of TYPE('a)) [True]"
+lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('a)) [True]"
apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
apply simp
apply (simp only: rtb_rbl_ariths(1)[OF refl])
@@ -79,22 +64,18 @@
apply (simp add: takefill_alt)
done
-lemma rbl_word_if:
- "rev (to_bl (if P then x else y))
- = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def split_def)
lemma rbl_add_carry_Cons:
- "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys))
- = xor3 x y car # (if carry x y car then rbl_succ else id)
- (rbl_add xs ys)"
+ "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
+ xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)"
by (simp add: carry_def xor3_def)
lemma rbl_add_suc_carry_fold:
"length xs = length ys \<Longrightarrow>
- \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys)
- = (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
- (zip xs ys) (\<lambda>_. [])) car"
+ \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) =
+ (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car"
apply (erule list_induct2)
apply simp
apply (simp only: rbl_add_carry_Cons)
@@ -102,84 +83,70 @@
done
lemma to_bl_plus_carry:
- "to_bl (x + y)
- = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
- (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
+ "to_bl (x + y) =
+ rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
+ (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
apply (simp add: word_add_rbl[OF refl refl])
apply (drule_tac x=False in spec)
apply (simp add: zip_rev)
done
-definition
- "rbl_plus cin xs ys = foldr
- (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
- (zip xs ys) (\<lambda>_. []) cin"
+definition "rbl_plus cin xs ys =
+ foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) cin"
lemma rbl_plus_simps:
- "rbl_plus cin (x # xs) (y # ys)
- = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
+ "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
"rbl_plus cin [] ys = []"
"rbl_plus cin xs [] = []"
by (simp_all add: rbl_plus_def)
-lemma rbl_word_plus:
- "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
-definition
- "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
+definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
lemma rbl_succ2_simps:
"rbl_succ2 b [] = []"
"rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
by (simp_all add: rbl_succ2_def)
-lemma twos_complement:
- "- x = word_succ (NOT x)"
+lemma twos_complement: "- x = word_succ (NOT x)"
using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
- by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1]
- del: word_add_not)
+ by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
-lemma rbl_word_neg:
- "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
- by (simp add: twos_complement word_succ_rbl[OF refl]
- bl_word_not rev_map rbl_succ2_def)
+lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
+ by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)
lemma rbl_word_cat:
- "rev (to_bl (word_cat x y :: ('a :: len0) word))
- = takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
+ "rev (to_bl (word_cat x y :: 'a::len0 word)) =
+ takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
by (simp add: word_cat_bl word_rev_tf)
lemma rbl_word_slice:
- "rev (to_bl (slice n w :: ('a :: len0) word))
- = takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
+ "rev (to_bl (slice n w :: 'a::len0 word)) =
+ takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
apply (simp add: slice_take word_rev_tf rev_take)
apply (cases "n < len_of TYPE('b)", simp_all)
done
lemma rbl_word_ucast:
- "rev (to_bl (ucast x :: ('a :: len0) word))
- = takefill False (len_of TYPE('a)) (rev (to_bl x))"
+ "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))"
apply (simp add: to_bl_ucast takefill_alt)
apply (simp add: rev_drop)
- apply (case_tac "len_of TYPE('a) < len_of TYPE('b)")
+ apply (cases "len_of TYPE('a) < len_of TYPE('b)")
apply simp_all
done
lemma rbl_shiftl:
- "rev (to_bl (w << n)) = takefill False (size w)
- (replicate n False @ rev (to_bl w))"
+ "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))"
by (simp add: bl_shiftl takefill_alt word_size rev_drop)
lemma rbl_shiftr:
- "rev (to_bl (w >> n)) = takefill False (size w)
- (drop n (rev (to_bl w)))"
+ "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))"
by (simp add: shiftr_slice rbl_word_slice word_size)
-definition
- "drop_nonempty v n xs
- = (if n < length xs then drop n xs else [last (v # xs)])"
+definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])"
lemma drop_nonempty_simps:
"drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
@@ -187,86 +154,69 @@
"drop_nonempty v n [] = [v]"
by (simp_all add: drop_nonempty_def)
-definition
- "takefill_last x n xs = takefill (last (x # xs)) n xs"
+definition "takefill_last x n xs = takefill (last (x # xs)) n xs"
lemma takefill_last_simps:
"takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
"takefill_last z 0 xs = []"
"takefill_last z n [] = replicate n z"
- apply (simp_all add: takefill_last_def)
- apply (simp_all add: takefill_alt)
- done
+ by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
lemma rbl_sshiftr:
- "rev (to_bl (w >>> n)) =
- takefill_last False (size w)
- (drop_nonempty False n (rev (to_bl w)))"
+ "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))"
apply (cases "n < size w")
apply (simp add: bl_sshiftr takefill_last_def word_size
- takefill_alt rev_take last_rev
- drop_nonempty_def)
+ takefill_alt rev_take last_rev
+ drop_nonempty_def)
apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
apply (simp add: word_size takefill_last_def takefill_alt
- last_rev word_msb_alt word_rev_tf
- drop_nonempty_def take_Cons')
+ last_rev word_msb_alt word_rev_tf
+ drop_nonempty_def take_Cons')
apply (case_tac "len_of TYPE('a)", simp_all)
apply (rule word_eqI)
apply (simp add: nth_sshiftr word_size test_bit_of_bl
- msb_nth)
+ msb_nth)
done
lemma nth_word_of_int:
- "(word_of_int x :: ('a :: len0) word) !! n
- = (n < len_of TYPE('a) \<and> bin_nth x n)"
+ "(word_of_int x :: 'a::len0 word) !! n = (n < len_of TYPE('a) \<and> bin_nth x n)"
apply (simp add: test_bit_bl word_size to_bl_of_bin)
apply (subst conj_cong[OF refl], erule bin_nth_bl)
- apply (auto)
+ apply auto
done
lemma nth_scast:
- "(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n
- = (n < len_of TYPE('b) \<and>
- (if n < len_of TYPE('a) - 1 then x !! n
- else x !! (len_of TYPE('a) - 1)))"
- by (simp add: scast_def nth_word_of_int nth_sint)
+ "(scast (x :: 'a::len word) :: 'b::len word) !! n =
+ (n < len_of TYPE('b) \<and>
+ (if n < len_of TYPE('a) - 1 then x !! n
+ else x !! (len_of TYPE('a) - 1)))"
+ by (simp add: scast_def nth_sint)
lemma rbl_word_scast:
- "rev (to_bl (scast x :: ('a :: len) word))
- = takefill_last False (len_of TYPE('a))
- (rev (to_bl x))"
+ "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))"
apply (rule nth_equalityI)
apply (simp add: word_size takefill_last_def)
apply (clarsimp simp: nth_scast takefill_last_def
- nth_takefill word_size nth_rev to_bl_nth)
+ nth_takefill word_size nth_rev to_bl_nth)
apply (cases "len_of TYPE('b)")
apply simp
apply (clarsimp simp: less_Suc_eq_le linorder_not_less
- last_rev word_msb_alt[symmetric]
- msb_nth)
+ last_rev word_msb_alt[symmetric]
+ msb_nth)
done
-definition
- rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
-where
- "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm))
- xs []"
+definition rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+ where "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm)) xs []"
lemma rbl_mul_simps:
- "rbl_mul (x # xs) ys
- = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
+ "rbl_mul (x # xs) ys = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
"rbl_mul [] ys = []"
by (simp_all add: rbl_mul_def)
-lemma takefill_le2:
- "length xs \<le> n \<Longrightarrow>
- takefill x m (takefill x n xs)
- = takefill x m xs"
+lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs"
by (simp add: takefill_alt replicate_add[symmetric])
-lemma take_rbl_plus:
- "\<forall>n b. take n (rbl_plus b xs ys)
- = rbl_plus b (take n xs) (take n ys)"
+lemma take_rbl_plus: "\<forall>n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)"
apply (simp add: rbl_plus_def take_zip[symmetric])
apply (rule_tac list="zip xs ys" in list.induct)
apply simp
@@ -275,52 +225,39 @@
done
lemma word_rbl_mul_induct:
- fixes y :: "'a :: len word" shows
- "length xs \<le> size y
- \<Longrightarrow> rbl_mul xs (rev (to_bl y))
- = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
+ "length xs \<le> size y \<Longrightarrow>
+ rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
+ for y :: "'a::len word"
proof (induct xs)
case Nil
- show ?case
- by (simp add: rbl_mul_simps)
+ show ?case by (simp add: rbl_mul_simps)
next
case (Cons z zs)
- have rbl_word_plus':
- "\<And>(x :: 'a word) y.
- to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
+ have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
+ for x y :: "'a word"
by (simp add: rbl_word_plus[symmetric])
-
+
have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)"
- apply (cases z)
- apply (simp cong: map_cong)
- apply (simp add: map_replicate_const cong: map_cong)
- done
-
- have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1"
+ by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
+
+ have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
by (simp add: shiftl_t2n)
- have zip_take_triv: "\<And>xs ys n. n = length ys
- \<Longrightarrow> zip (take n xs) ys = zip xs ys"
- by (rule nth_equalityI, simp_all)
+ have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys"
+ by (rule nth_equalityI) simp_all
- show ?case
- using Cons
+ from Cons show ?case
apply (simp add: trans [OF of_bl_append add.commute]
- rbl_mul_simps rbl_word_plus'
- Cons.hyps distrib_right mult_bit
- shiftl rbl_shiftl)
- apply (simp add: takefill_alt word_size rev_map take_rbl_plus
- min_def)
+ rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl)
+ apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def)
apply (simp add: rbl_plus_def zip_take_triv)
done
qed
-lemma rbl_word_mul:
- fixes x :: "'a :: len word"
- shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
- using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
- by (simp add: word_size)
+lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
+ for x :: "'a::len word"
+ using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
text \<open>Breaking up inequalities into bitlist properties.\<close>
@@ -333,9 +270,8 @@
lemma rev_bl_order_simps:
"rev_bl_order F [] [] = F"
- "rev_bl_order F (x # xs) (y # ys)
- = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
- apply (simp_all add: rev_bl_order_def)
+ "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
+ apply (simp_all add: rev_bl_order_def)
apply (rule conj_cong[OF refl])
apply (cases "xs = ys")
apply (simp add: nth_Cons')
@@ -350,39 +286,30 @@
lemma rev_bl_order_rev_simp:
"length xs = length ys \<Longrightarrow>
- rev_bl_order F (xs @ [x]) (ys @ [y])
- = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
- apply (induct arbitrary: F rule: list_induct2)
- apply (auto simp add: rev_bl_order_simps)
- done
+ rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
+ by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
lemma rev_bl_order_bl_to_bin:
- "length xs = length ys
- \<Longrightarrow> rev_bl_order True xs ys
- = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys))
- \<and> rev_bl_order False xs ys
- = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
+ "length xs = length ys \<Longrightarrow>
+ rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and>
+ rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
apply (induct xs ys rule: list_induct2)
apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
done
-lemma word_le_rbl:
- fixes x :: "('a :: len0) word"
- shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
+lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
+ for x y :: "'a::len0 word"
by (simp add: rev_bl_order_bl_to_bin word_le_def)
-lemma word_less_rbl:
- fixes x :: "('a :: len0) word"
- shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
+lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
+ for x y :: "'a::len0 word"
by (simp add: word_less_alt rev_bl_order_bl_to_bin)
-lemma word_sint_msb_eq:
- "sint x = uint x - (if msb x then 2 ^ size x else 0)"
+lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
apply (cases "msb x")
apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
- apply (simp add: word_size wi_hom_syms
- word_of_int_2p_len)
+ apply (simp add: word_size wi_hom_syms word_of_int_2p_len)
apply (simp add: sints_num word_size)
apply (rule conjI)
apply (simp add: le_diff_eq')
@@ -398,11 +325,8 @@
apply simp
done
-lemma word_sle_msb_le:
- "(x <=s y) = ((msb y --> msb x) \<and>
- ((msb x \<and> \<not> msb y) \<or> (x <= y)))"
- apply (simp add: word_sle_def word_sint_msb_eq word_size
- word_le_def)
+lemma word_sle_msb_le: "x <=s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)"
+ apply (simp add: word_sle_def word_sint_msb_eq word_size word_le_def)
apply safe
apply (rule order_trans[OF _ uint_ge_0])
apply (simp add: order_less_imp_le)
@@ -411,13 +335,10 @@
apply simp
done
-lemma word_sless_msb_less:
- "(x <s y) = ((msb y --> msb x) \<and>
- ((msb x \<and> \<not> msb y) \<or> (x < y)))"
+lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)"
by (auto simp add: word_sless_def word_sle_msb_le)
-definition
- "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
+definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
lemma map_last_simps:
"map_last f [] = []"
@@ -426,8 +347,7 @@
by (simp_all add: map_last_def)
lemma word_sle_rbl:
- "(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x)))
- (map_last Not (rev (to_bl y)))"
+ "x <=s y \<longleftrightarrow> rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
using word_msb_alt[where w=x] word_msb_alt[where w=y]
apply (simp add: word_sle_msb_le word_le_rbl)
apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
@@ -438,8 +358,7 @@
done
lemma word_sless_rbl:
- "(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x)))
- (map_last Not (rev (to_bl y)))"
+ "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
using word_msb_alt[where w=x] word_msb_alt[where w=y]
apply (simp add: word_sless_msb_less word_less_rbl)
apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
@@ -450,51 +369,45 @@
done
text \<open>Lemmas for unpacking rev (to_bl n) for numerals n and also
-for irreducible values and expressions.\<close>
+ for irreducible values and expressions.\<close>
lemma rev_bin_to_bl_simps:
"rev (bin_to_bl 0 x) = []"
- "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
- = False # rev (bin_to_bl n (numeral nm))"
- "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm)))
- = True # rev (bin_to_bl n (numeral nm))"
- "rev (bin_to_bl (Suc n) (numeral (num.One)))
- = True # replicate n False"
- "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
- = False # rev (bin_to_bl n (- numeral nm))"
- "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
- = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
- "rev (bin_to_bl (Suc n) (- numeral (num.One)))
- = True # replicate n True"
- "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
- = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
- "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
- = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
- "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
- = False # rev (bin_to_bl n (- numeral num.One))"
- apply (simp_all add: bin_to_bl_def)
+ "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))"
+ "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))"
+ "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) =
+ True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
+ True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
+ False # rev (bin_to_bl n (- numeral (nm + num.One)))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
+ False # rev (bin_to_bl n (- numeral num.One))"
+ apply simp_all
apply (simp_all only: bin_to_bl_aux_alt)
apply (simp_all)
apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
done
-lemma to_bl_upt:
- "to_bl x = rev (map (op !! x) [0 ..< size x])"
+lemma to_bl_upt: "to_bl x = rev (map (op !! x) [0 ..< size x])"
apply (rule nth_equalityI)
apply (simp add: word_size)
- apply (clarsimp simp: to_bl_nth word_size nth_rev)
+ apply (auto simp: to_bl_nth word_size nth_rev)
done
-lemma rev_to_bl_upt:
- "rev (to_bl x) = map (op !! x) [0 ..< size x]"
+lemma rev_to_bl_upt: "rev (to_bl x) = map (op !! x) [0 ..< size x]"
by (simp add: to_bl_upt)
lemma upt_eq_list_intros:
- "j <= i \<Longrightarrow> [i ..< j] = []"
- "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
- by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
+ "j \<le> i \<Longrightarrow> [i ..< j] = []"
+ "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
+ by (simp_all add: upt_eq_Cons_conv)
-text \<open>Tactic definition\<close>
+
+subsection \<open>Tactic definition\<close>
ML \<open>
structure Word_Bitwise_Tac =
@@ -517,7 +430,7 @@
|> Thm.apply @{cterm Trueprop};
in
try (fn () =>
- Goal.prove_internal ctxt [] prop
+ Goal.prove_internal ctxt [] prop
(K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
end
@@ -616,7 +529,6 @@
end;
end
-
\<close>
method_setup word_bitwise =
--- a/src/HOL/Word/Word_Miscellaneous.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1,34 +1,27 @@
-(* Title: HOL/Word/Word_Miscellaneous.thy
- Author: Miscellaneous
-*)
+(* Title: HOL/Word/Word_Miscellaneous.thy *)
section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
theory Word_Miscellaneous
-imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
+ imports "~~/src/HOL/Library/Bit" Misc_Numeric
begin
-lemma power_minus_simp:
- "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
+lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
by (auto dest: gr0_implies_Suc)
-lemma funpow_minus_simp:
- "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
+lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
by (auto dest: gr0_implies_Suc)
-lemma power_numeral:
- "a ^ numeral k = a * a ^ (pred_numeral k)"
+lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)"
by (simp add: numeral_eq_Suc)
-lemma funpow_numeral [simp]:
- "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
+lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
by (simp add: numeral_eq_Suc)
-lemma replicate_numeral [simp]:
- "replicate (numeral k) x = x # replicate (pred_numeral k) x"
+lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"
by (simp add: numeral_eq_Suc)
-lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n"
+lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n"
apply (rule ext)
apply (induct n)
apply (simp_all add: o_def)
@@ -37,7 +30,8 @@
lemma list_exhaust_size_gt0:
assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
shows "0 < length y \<Longrightarrow> P"
- apply (cases y, simp)
+ apply (cases y)
+ apply simp
apply (rule y)
apply fastforce
done
@@ -46,22 +40,24 @@
assumes y: "y = [] \<Longrightarrow> P"
shows "length y = 0 \<Longrightarrow> P"
apply (cases y)
- apply (rule y, simp)
+ apply (rule y)
+ apply simp
apply simp
done
-lemma size_Cons_lem_eq:
- "y = xa # list ==> size y = Suc k ==> size list = k"
+lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k"
by auto
lemmas ls_splits = prod.split prod.split_asm if_split_asm
-lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
+lemma not_B1_is_B0: "y \<noteq> 1 \<Longrightarrow> y = 0"
+ for y :: bit
by (cases y) auto
-lemma B1_ass_B0:
- assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)"
- shows "y = (1::bit)"
+lemma B1_ass_B0:
+ fixes y :: bit
+ assumes y: "y = 0 \<Longrightarrow> y = 1"
+ shows "y = 1"
apply (rule classical)
apply (drule not_B1_is_B0)
apply (erule y)
@@ -72,7 +68,7 @@
lemmas s2n_ths = n2s_ths [symmetric]
-lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
+lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys"
by auto
lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
@@ -84,20 +80,19 @@
lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
by auto
-lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
+lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))"
by auto
-lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
+lemma if_x_Not: "(if p then x else \<not> x) = (p = x)"
by auto
-lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
+lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)"
by auto
-lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))"
+lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = u else y = v)"
by auto
-lemma if_same_eq_not:
- "(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))"
+lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
by auto
(* note - if_Cons can cause blowup in the size, if p is complex,
@@ -105,25 +100,28 @@
lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
by auto
-lemma if_single:
- "(if xc then [xab] else [an]) = [if xc then xab else an]"
+lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]"
by auto
lemma if_bool_simps:
- "If p True y = (p | y) & If p False y = (~p & y) &
- If p y True = (p --> y) & If p y False = (p & y)"
+ "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>
+ If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)"
by auto
-lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
+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"] for w (* FIXME: delete *)
-lemma the_elemI: "y = {x} ==> the_elem y = x"
+lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x"
by simp
-lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
+lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R"
+ by auto
-lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith
+lemma gt_or_eq_0: "0 < y \<or> 0 = y"
+ for y :: nat
+ by arith
lemmas xtr1 = xtrans(1)
lemmas xtr2 = xtrans(2)
@@ -137,63 +135,76 @@
lemmas nat_simps = diff_add_inverse2 diff_add_inverse
lemmas nat_iffs = le_add1 le_add2
-lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith
+lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k"
+ for k :: nat
+ by arith
lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
-lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
+lemma nmod2: "n mod 2 = 0 \<or> n mod 2 = 1"
+ for n :: int
by arith
lemmas eme1p = emep1 [simplified add.commute]
-lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))" by arith
+lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c"
+ for a b c :: int
+ by arith
-lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith
+lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c"
+ for a b c :: int
+ by arith
-lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith
+lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c"
+ for a b c :: int
+ by arith
lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
-lemma z1pdiv2:
- "(2 * b + 1) div 2 = (b::int)" by arith
+lemma z1pdiv2: "(2 * b + 1) div 2 = b"
+ for b :: int
+ by arith
lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
simplified int_one_le_iff_zero_less, simplified]
-
-lemma axxbyy:
- "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>
- a = b & m = (n :: int)" by arith
-lemma axxmod2:
- "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith
+lemma axxbyy: "a + m + m = b + n + n \<Longrightarrow> a = 0 \<or> a = 1 \<Longrightarrow> b = 0 \<or> b = 1 \<Longrightarrow> a = b \<and> m = n"
+ for a b m n :: int
+ by arith
+
+lemma axxmod2: "(1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0"
+ for x :: int
+ by arith
-lemma axxdiv2:
- "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)" by arith
+lemma axxdiv2: "(1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x"
+ for x :: int
+ by arith
-lemmas iszero_minus = trans [THEN trans,
- OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]]
+lemmas iszero_minus =
+ trans [THEN trans, OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]]
-lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add.commute]
+lemmas zadd_diff_inverse =
+ trans [OF diff_add_cancel [symmetric] add.commute]
-lemmas add_diff_cancel2 = add.commute [THEN diff_eq_eq [THEN iffD2]]
+lemmas add_diff_cancel2 =
+ add.commute [THEN diff_eq_eq [THEN iffD2]]
lemmas rdmods [symmetric] = mod_minus_eq
mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
mod_add_right_eq mod_mult_right_eq mod_mult_left_eq
-lemma mod_plus_right:
- "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
- apply (induct x)
- apply (simp_all add: mod_Suc)
- apply arith
- done
+lemma mod_plus_right: "(a + x) mod m = (b + x) mod m \<longleftrightarrow> a mod m = b mod m"
+ for a b m x :: nat
+ by (induct x) (simp_all add: mod_Suc, arith)
-lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)"
- by (induct n) (simp_all add : mod_Suc)
+lemma nat_minus_mod: "(n - n mod m) mod m = 0"
+ for m n :: nat
+ by (induct n) (simp_all add: mod_Suc)
-lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
- THEN mod_plus_right [THEN iffD2], simplified]
+lemmas nat_minus_mod_plus_right =
+ trans [OF nat_minus_mod mod_0 [symmetric],
+ THEN mod_plus_right [THEN iffD2], simplified]
lemmas push_mods' = mod_add_eq
mod_mult_eq mod_diff_eq
@@ -202,23 +213,22 @@
lemmas push_mods = push_mods' [THEN eq_reflection]
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
-lemma nat_mod_eq:
- "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"
+lemma nat_mod_eq: "b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
+ for a b n :: nat
by (induct a) auto
lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
-lemma nat_mod_lem:
- "(0 :: nat) < n ==> b < n = (b mod n = b)"
+lemma nat_mod_lem: "0 < n \<Longrightarrow> b < n \<longleftrightarrow> b mod n = b"
+ for b n :: nat
apply safe
apply (erule nat_mod_eq')
apply (erule subst)
apply (erule mod_less_divisor)
done
-lemma mod_nat_add:
- "(x :: nat) < z ==> y < z ==>
- (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+lemma mod_nat_add: "x < z \<Longrightarrow> y < z \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+ for x y z :: nat
apply (rule nat_mod_eq)
apply auto
apply (rule trans)
@@ -228,42 +238,46 @@
apply arith
done
-lemma mod_nat_sub:
- "(x :: nat) < z ==> (x - y) mod z = x - y"
+lemma mod_nat_sub: "x < z \<Longrightarrow> (x - y) mod z = x - y"
+ for x y :: nat
by (rule nat_mod_eq') arith
-lemma int_mod_eq:
- "(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
+lemma int_mod_eq: "0 \<le> b \<Longrightarrow> b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
+ for a b n :: int
by (metis mod_pos_pos_trivial)
lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
-lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
+lemma int_mod_le: "0 \<le> a \<Longrightarrow> a mod n \<le> a"
+ for a :: int
by (fact Divides.semiring_numeral_div_class.mod_less_eq_dividend) (* FIXME: delete *)
lemma mod_add_if_z:
- "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
- (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+ "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+ (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+ for x y z :: int
by (auto intro: int_mod_eq)
lemma mod_sub_if_z:
- "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
- (x - y) mod z = (if y <= x then x - y else x - y + z)"
+ "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+ (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
+ for x y z :: int
by (auto intro: int_mod_eq)
lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric]
lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
(* already have this for naturals, div_mult_self1/2, but not for ints *)
-lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n"
+lemma zdiv_mult_self: "m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n"
+ for a m n :: int
apply (rule mcl)
prefer 2
apply (erule asm_rl)
apply (simp add: zmde ring_distribs)
done
-lemma mod_power_lem:
- "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
+lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
+ for a :: int
apply clarsimp
apply safe
apply (simp add: dvd_eq_mod_eq_0 [symmetric])
@@ -275,15 +289,19 @@
apply auto
done
-lemma pl_pl_rels:
- "a + b = c + d ==>
- a >= c & b <= d | a <= c & b >= (d :: nat)" by arith
+lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
+ for a b c d :: nat
+ by arith
lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels]
-lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))" by arith
+lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0"
+ for k m :: nat
+ by arith
-lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b" by arith
+lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b"
+ for a b c d :: nat
+ by arith
lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
@@ -291,33 +309,37 @@
lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
-lemma td_gal:
- "0 < c ==> (a >= b * c) = (a div c >= (b :: nat))"
+lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
+ for a b c :: nat
apply safe
apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])
apply (erule th2)
done
-
+
lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
-lemma div_mult_le: "(a :: nat) div b * b <= a"
+lemma div_mult_le: "a div b * b \<le> a"
+ for a b :: nat
by (fact dtle)
lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
-lemma given_quot: "f > (0 :: nat) ==> (f * l + (f - 1)) div f = l"
+lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
+ for f l :: nat
by (rule sdl, assumption) (simp (no_asm))
-lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f - Suc 0) div f = l"
+lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
+ for f l :: nat
apply (frule given_quot)
apply (rule trans)
prefer 2
apply (erule asm_rl)
- apply (rule_tac f="%n. n div f" in arg_cong)
+ apply (rule_tac f="\<lambda>n. n div f" in arg_cong)
apply (simp add : ac_simps)
done
-
-lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
+
+lemma diff_mod_le: "a < d \<Longrightarrow> b dvd d \<Longrightarrow> a - a mod b \<le> d - b"
+ for a b d :: nat
apply (unfold dvd_def)
apply clarify
apply (case_tac k)
@@ -332,57 +354,56 @@
apply auto
done
-lemma less_le_mult':
- "w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)"
+lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c"
+ for b c w :: int
apply (rule mult_right_mono)
apply (rule zless_imp_add1_zle)
apply (erule (1) mult_right_less_imp_less)
apply assumption
done
-lemma less_le_mult:
- "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * (c::int)"
+lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c"
+ for b c w :: int
using less_le_mult' [of w c b] by (simp add: algebra_simps)
-lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
+lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
simplified left_diff_distrib]
-lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))"
+lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))"
by auto
-lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i" by arith
+lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i"
+ for i j k :: nat
+ by arith
-lemma nonneg_mod_div:
- "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b"
- apply (cases "b = 0", clarsimp)
- apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
- done
+lemma nonneg_mod_div: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> (a mod b) \<and> 0 \<le> a div b"
+ for a b :: int
+ by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
declare iszero_0 [intro]
-lemma min_pm [simp]:
- "min a b + (a - b) = (a :: nat)"
+lemma min_pm [simp]: "min a b + (a - b) = a"
+ for a b :: nat
by arith
-
-lemma min_pm1 [simp]:
- "a - b + min a b = (a :: nat)"
+
+lemma min_pm1 [simp]: "a - b + min a b = a"
+ for a b :: nat
by arith
-lemma rev_min_pm [simp]:
- "min b a + (a - b) = (a :: nat)"
+lemma rev_min_pm [simp]: "min b a + (a - b) = a"
+ for a b :: nat
by arith
-lemma rev_min_pm1 [simp]:
- "a - b + min b a = (a :: nat)"
+lemma rev_min_pm1 [simp]: "a - b + min b a = a"
+ for a b :: nat
by arith
-lemma min_minus [simp]:
- "min m (m - k) = (m - k :: nat)"
+lemma min_minus [simp]: "min m (m - k) = m - k"
+ for m k :: nat
by arith
-
-lemma min_minus' [simp]:
- "min (m - k) m = (m - k :: nat)"
+
+lemma min_minus' [simp]: "min (m - k) m = m - k"
+ for m k :: nat
by arith
end
-
--- a/src/Pure/General/long_name.ML Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/General/long_name.ML Mon Apr 03 23:12:44 2017 +0200
@@ -64,4 +64,3 @@
in implode (nth_map (length names - 1) f names) end;
end;
-
--- a/src/Pure/General/long_name.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/General/long_name.scala Mon Apr 03 23:12:44 2017 +0200
@@ -25,4 +25,3 @@
if (name == "") ""
else explode(name).last
}
-
--- a/src/Pure/PIDE/command.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/command.scala Mon Apr 03 23:12:44 2017 +0200
@@ -435,7 +435,7 @@
// inlined errors
case Thy_Header.THEORY =>
val reader = Scan.char_reader(Token.implode(span.content))
- val header = resources.check_thy_reader("", node_name, reader)
+ val header = resources.check_thy_reader(node_name, reader)
val errors =
for ((imp, pos) <- header.imports if !can_import(imp)) yield {
val msg =
--- a/src/Pure/PIDE/document.ML Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/document.ML Mon Apr 03 23:12:44 2017 +0200
@@ -178,9 +178,7 @@
| NONE => false);
fun loaded_theory name =
- (case try (unsuffix ".thy") name of
- SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
- | NONE => NONE);
+ get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
fun get_node nodes name = String_Graph.get_node nodes name
handle String_Graph.UNDEF _ => empty_node;
--- a/src/Pure/PIDE/document.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/document.scala Mon Apr 03 23:12:44 2017 +0200
@@ -98,6 +98,7 @@
object Name
{
val empty = Name("")
+ def theory(theory: String): Name = Name(theory, "", theory)
object Ordering extends scala.math.Ordering[Name]
{
@@ -486,12 +487,12 @@
def is_stable: Boolean
def snapshot(): Snapshot
- def node_name: Document.Node.Name
+ def node_name: Node.Name
def is_theory: Boolean = node_name.is_theory
override def toString: String = node_name.toString
def node_required: Boolean
- def get_blob: Option[Document.Blob]
+ def get_blob: Option[Blob]
def node_edits(
node_header: Node.Header,
@@ -502,13 +503,12 @@
get_blob match {
case None =>
List(
- Document.Node.Deps(
- if (session.resources.base.loaded_theories(node_name.theory))
+ Node.Deps(
+ if (session.resources.session_base.loaded_theory(node_name))
node_header.error("Cannot update finished theory " + quote(node_name.theory))
else node_header),
- Document.Node.Edits(text_edits), perspective)
- case Some(blob) =>
- List(Document.Node.Blob(blob), Document.Node.Edits(text_edits))
+ Node.Edits(text_edits), perspective)
+ case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))
}
edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
}
--- a/src/Pure/PIDE/resources.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 03 23:12:44 2017 +0200
@@ -13,26 +13,16 @@
import java.io.{File => JFile}
-class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
+class Resources(
+ val session_name: String,
+ val session_base: Sessions.Base,
+ val log: Logger = No_Logger)
{
val thy_info = new Thy_Info(this)
def thy_path(path: Path): Path = path.ext("thy")
- /* document node names */
-
- def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
- {
- val no_qualifier = "" // FIXME
- val path = raw_path.expand
- val node = path.implode
- val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
- val master_dir = if (theory == "") "" else path.dir.implode
- Document.Node.Name(node, master_dir, theory)
- }
-
-
/* file-system operations */
def append(dir: String, source_path: Path): String =
@@ -77,28 +67,38 @@
}
else Nil
- private def dummy_name(theory: String): Document.Node.Name =
- Document.Node.Name(theory + ".thy", "", theory)
+ def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
+ {
+ val path = raw_path.expand
+ val node = path.implode
+ val qualifier = if (global) "" else session_name
+ val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+ val master_dir = if (theory == "") "" else path.dir.implode
+ Document.Node.Name(node, master_dir, theory)
+ }
- def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
+ def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
{
- val no_qualifier = "" // FIXME
- val thy1 = Thy_Header.base_name(s)
- val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
- (base.known_theories.get(thy1) orElse
- base.known_theories.get(thy2) orElse
- base.known_theories.get(Long_Name.base_name(thy1))) match {
- case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
+ val theory = Thy_Header.base_name(s)
+ val is_base_name = Thy_Header.is_base_name(s)
+ val is_qualified = is_base_name && Long_Name.is_qualified(s)
+
+ val known_theory =
+ if (is_base_name)
+ session_base.known_theories.get(theory) orElse
+ (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
+ else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
+ else None
+
+ known_theory match {
+ case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
case Some(name) => name
+ case None if is_qualified => Document.Node.Name.theory(theory)
case None =>
val path = Path.explode(s)
- val theory = path.base.implode
- if (Long_Name.is_qualified(theory)) dummy_name(theory)
- else {
- val node = append(master.master_dir, thy_path(path))
- val master_dir = append(master.master_dir, path.dir)
- Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
- }
+ val node = append(master.master_dir, thy_path(path))
+ val master_dir = append(master.master_dir, path.dir)
+ Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
}
}
@@ -111,9 +111,8 @@
try { f(reader) } finally { reader.close }
}
- def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
- reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
- : Document.Node.Header =
+ def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
+ start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
{
if (node_name.is_theory && reader.source.length > 0) {
try {
@@ -127,7 +126,7 @@
Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
val imports =
- header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
+ header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
Document.Node.Header(imports, header.keywords, header.abbrevs)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -135,18 +134,18 @@
else Document.Node.no_header
}
- def check_thy(qualifier: String, name: Document.Node.Name,
- start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
- with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
+ def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
+ strict: Boolean = true): Document.Node.Header =
+ with_thy_reader(name, check_thy_reader(name, _, start, strict))
/* special header */
def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
if (Thy_Header.is_ml_root(name.theory))
- Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
+ Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
else if (Thy_Header.is_bootstrap(name.theory))
- Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
+ Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
else None
@@ -155,7 +154,7 @@
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
(for {
(node_name, node) <- nodes.iterator
- if !base.loaded_theories(node_name.theory)
+ if !session_base.loaded_theory(node_name)
cmd <- node.load_commands.iterator
name <- cmd.blobs_undefined.iterator
} yield name).toList
--- a/src/Pure/PIDE/session.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/session.scala Mon Apr 03 23:12:44 2017 +0200
@@ -191,7 +191,7 @@
def recent_syntax(name: Document.Node.Name): Outer_Syntax =
global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
- resources.base.syntax
+ resources.session_base.syntax
/* pipelined change parsing */
--- a/src/Pure/Thy/sessions.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 03 23:12:44 2017 +0200
@@ -17,25 +17,14 @@
object Sessions
{
- /* Pure */
-
- def pure_name(name: String): Boolean = name == Thy_Header.PURE
+ /* base info and source dependencies */
- def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
- {
- val roots = Thy_Header.ml_roots.map(_._1)
- val loaded_files =
- roots.flatMap(root => resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
- (roots ::: loaded_files).map(file => dir + Path.explode(file))
- }
-
- def pure_base(options: Options): Base = session_base(options, Thy_Header.PURE)
-
-
- /* base info and source dependencies */
+ def is_pure(name: String): Boolean = name == Thy_Header.PURE
object Base
{
+ def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+
lazy val bootstrap: Base =
Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
}
@@ -47,6 +36,10 @@
syntax: Outer_Syntax = Outer_Syntax.empty,
sources: List[(Path, SHA1.Digest)] = Nil,
session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+ {
+ def loaded_theory(name: Document.Node.Name): Boolean =
+ loaded_theories.contains(name.theory)
+ }
sealed case class Deps(deps: Map[String, Base])
{
@@ -67,12 +60,12 @@
if (progress.stopped) throw Exn.Interrupt()
try {
- val resources =
- new Resources(
- info.parent match {
- case None => Base.bootstrap
- case Some(parent) => deps(parent)
- })
+ val parent_base =
+ info.parent match {
+ case None => Base.bootstrap
+ case Some(parent) => deps(parent)
+ }
+ val resources = new Resources(name, parent_base)
if (verbose || list_files) {
val groups =
@@ -87,10 +80,9 @@
info.theories.flatMap({
case (global, _, thys) =>
thys.map(thy =>
- (resources.node_name(
- if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
+ (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
})
- val thy_deps = resources.thy_info.dependencies(name, root_theories)
+ val thy_deps = resources.thy_info.dependencies(root_theories)
thy_deps.errors match {
case Nil => thy_deps
@@ -99,7 +91,7 @@
}
val known_theories =
- (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
+ (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) =>
val name = dep.name
known.get(name.theory) match {
case Some(name1) if name != name1 =>
@@ -117,7 +109,13 @@
val loaded_files =
if (inlined_files) {
val pure_files =
- if (pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
+ if (is_pure(name)) {
+ val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
+ val files =
+ roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
+ map(file => info.dir + Path.explode(file))
+ roots ::: files
+ }
else Nil
pure_files ::: thy_deps.loaded_files
}
@@ -138,7 +136,7 @@
val session_graph =
Present.session_graph(info.parent getOrElse "",
- resources.base.loaded_theories, thy_deps.deps)
+ parent_base.loaded_theories, thy_deps.deps)
val base =
Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
@@ -365,8 +363,8 @@
val name = entry.name
if (name == "") error("Bad session name")
- if (pure_name(name) && entry.parent.isDefined) error("Illegal parent session")
- if (!pure_name(name) && !entry.parent.isDefined) error("Missing parent session")
+ if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+ if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
val session_options = options ++ entry.options
--- a/src/Pure/Thy/thy_header.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Apr 03 23:12:44 2017 +0200
@@ -80,6 +80,9 @@
private val Base_Name = new Regex(""".*?([^/\\:]+)""")
private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+ def is_base_name(s: String): Boolean =
+ s != "" && !s.exists("/\\:".contains(_))
+
def base_name(s: String): String =
s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
--- a/src/Pure/Thy/thy_info.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Mon Apr 03 23:12:44 2017 +0200
@@ -71,7 +71,7 @@
val import_errors =
(for {
(theory, names) <- seen_names.iterator_list
- if !resources.base.loaded_theories(theory)
+ if !resources.session_base.loaded_theories(theory)
if names.length > 1
} yield
"Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -83,10 +83,12 @@
}
lazy val syntax: Outer_Syntax =
- resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+ resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
def loaded_theories: Set[String] =
- (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
+ (resources.session_base.loaded_theories /: rev_deps) {
+ case (loaded, dep) => loaded + dep.name.theory
+ }
def loaded_files: List[Path] =
{
@@ -104,12 +106,12 @@
override def toString: String = deps.toString
}
- private def require_thys(session: String, initiators: List[Document.Node.Name],
- required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- (required /: thys)(require_thy(session, initiators, _, _))
+ private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
+ thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+ (required /: thys)(require_thy(initiators, _, _))
- private def require_thy(session: String, initiators: List[Document.Node.Name],
- required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
+ private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
+ thy: (Document.Node.Name, Position.T)): Dependencies =
{
val (name, require_pos) = thy
@@ -118,15 +120,14 @@
required_by(initiators) + Position.here(require_pos)
val required1 = required + thy
- if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
+ if (required.seen(name) || resources.session_base.loaded_theory(name)) required1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
val header =
- try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
+ try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
- Thy_Info.Dep(name, header) ::
- require_thys(session, name :: initiators, required1, header.imports)
+ Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
}
catch {
case e: Throwable =>
@@ -135,6 +136,6 @@
}
}
- def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- require_thys(session, Nil, Dependencies.empty, thys)
+ def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+ require_thys(Nil, Dependencies.empty, thys)
}
--- a/src/Pure/Thy/thy_syntax.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Apr 03 23:12:44 2017 +0200
@@ -101,7 +101,7 @@
else {
val header = node.header
val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
- Some((resources.base.syntax /: imports_syntax)(_ ++ _)
+ Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
.add_keywords(header.keywords).add_abbrevs(header.abbrevs))
}
nodes += (name -> node.update_syntax(syntax))
@@ -300,7 +300,7 @@
doc_blobs.get(name) orElse previous.nodes(name).get_blob
def can_import(name: Document.Node.Name): Boolean =
- resources.base.loaded_theories(name.theory) || nodes0(name).has_header
+ resources.session_base.loaded_theory(name) || nodes0(name).has_header
val (doc_edits, version) =
if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -324,7 +324,7 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
- val syntax = node.syntax getOrElse resources.base.syntax
+ val syntax = node.syntax getOrElse resources.session_base.syntax
val commands = node.commands
val node1 =
--- a/src/Pure/Tools/build.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Tools/build.scala Mon Apr 03 23:12:44 2017 +0200
@@ -219,8 +219,8 @@
"ML_Heap.share_common_data (); ML_Heap.save_child " +
ML_Syntax.print_string0(File.platform_path(output))
- if (pide && !Sessions.pure_name(name)) {
- val resources = new Resources(deps(parent))
+ if (pide && !Sessions.is_pure(name)) {
+ val resources = new Resources(name, deps(parent))
val session = new Session(options, resources)
val handler = new Handler(progress, session, name)
session.init_protocol_handler(handler)
@@ -255,7 +255,7 @@
(if (do_output) "; " + save_heap else "") + "));"
val process =
- if (Sessions.pure_name(name)) {
+ if (Sessions.is_pure(name)) {
ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
args =
(for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
@@ -519,7 +519,7 @@
val ancestor_results = selected_tree.ancestors(name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
- val do_output = build_heap || Sessions.pure_name(name) || queue.is_inner(name)
+ val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
val (current, heap_stamp) =
{
--- a/src/Tools/VSCode/src/document_model.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala Mon Apr 03 23:12:44 2017 +0200
@@ -73,7 +73,7 @@
def node_header: Document.Node.Header =
resources.special_header(node_name) getOrElse
- resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
+ resources.check_thy_reader(node_name, Scan.char_reader(content.text))
/* perspective */
--- a/src/Tools/VSCode/src/server.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Mon Apr 03 23:12:44 2017 +0200
@@ -225,8 +225,8 @@
}
}
- val base = Sessions.session_base(options, session_name, session_dirs)
- val resources = new VSCode_Resources(options, base, log)
+ val session_base = Sessions.session_base(options, session_name, session_dirs)
+ val resources = new VSCode_Resources(options, session_base, log)
{
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Apr 03 23:12:44 2017 +0200
@@ -40,9 +40,10 @@
}
class VSCode_Resources(
- val options: Options,
- base: Sessions.Base,
- log: Logger = No_Logger) extends Resources(base, log)
+ val options: Options,
+ session_base: Sessions.Base,
+ log: Logger = No_Logger)
+ extends Resources(session_name = "", session_base, log)
{
private val state = Synchronized(VSCode_Resources.State())
@@ -165,7 +166,7 @@
(for ((_, model) <- st.models.iterator if model.is_theory)
yield (model.node_name, Position.none)).toList
- val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
+ val thy_files = thy_info.dependencies(thys).deps.map(_.name)
/* auxiliary files */
--- a/src/Tools/jEdit/src/document_model.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Apr 03 23:12:44 2017 +0200
@@ -235,7 +235,7 @@
val pending_nodes = for ((node_name, None) <- purged) yield node_name
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
}
- val retain = PIDE.resources.thy_info.dependencies("", imports).deps.map(_.name).toSet
+ val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
yield edit
@@ -331,7 +331,7 @@
def node_header: Document.Node.Header =
PIDE.resources.special_header(node_name) getOrElse
- PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
+ PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
/* content */
@@ -396,8 +396,7 @@
PIDE.resources.special_header(node_name) getOrElse
JEdit_Lib.buffer_lock(buffer) {
- PIDE.resources.check_thy_reader(
- "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
+ PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
}
}
--- a/src/Tools/jEdit/src/isabelle.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Apr 03 23:12:44 2017 +0200
@@ -50,7 +50,7 @@
def mode_syntax(mode: String): Option[Outer_Syntax] =
mode match {
- case "isabelle" => Some(PIDE.resources.base.syntax)
+ case "isabelle" => Some(PIDE.resources.session_base.syntax)
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Sessions.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Apr 03 23:12:44 2017 +0200
@@ -21,7 +21,8 @@
import org.gjt.sp.jedit.bufferio.BufferIORequest
-class JEdit_Resources(base: Sessions.Base) extends Resources(base)
+class JEdit_Resources(session_base: Sessions.Base)
+ extends Resources(session_name = "", session_base)
{
/* document node name */
--- a/src/Tools/jEdit/src/plugin.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Apr 03 23:12:44 2017 +0200
@@ -74,7 +74,7 @@
val session_name = JEdit_Sessions.session_name(options)
val session_base =
try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
- catch { case ERROR(_) => Sessions.pure_base(options) }
+ catch { case ERROR(_) => Sessions.Base.pure(options) }
_resources =
new JEdit_Resources(session_base.copy(known_theories =
@@ -135,7 +135,7 @@
val thys =
(for ((node_name, model) <- models.iterator if model.is_theory)
yield (node_name, Position.none)).toList
- val thy_files = resources.thy_info.dependencies("", thys).deps.map(_.name)
+ val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
val aux_files =
if (options.bool("jedit_auto_resolve")) {
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Apr 03 23:12:44 2017 +0200
@@ -192,7 +192,7 @@
}
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
+ if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
status
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
--- a/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Apr 03 23:12:44 2017 +0200
@@ -187,7 +187,7 @@
}
val nodes_timing1 =
(nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.resources.base.loaded_theories(name.theory)) timing1
+ if (PIDE.resources.session_base.loaded_theory(name)) timing1
else {
val node_timing =
Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)