author | haftmann |
Tue, 19 Nov 2013 10:05:53 +0100 | |
changeset 54489 | 03ff4d1e6784 |
parent 54230 | b1d955791529 |
child 54847 | d6cf9a5b9be9 |
permissions | -rw-r--r-- |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
1 |
(* Title: HOL/Word/WordBitwise.thy |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
2 |
Authors: Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
3 |
*) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
4 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
5 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
6 |
theory WordBitwise |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
7 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
8 |
imports Word |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
9 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
10 |
begin |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
11 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
12 |
text {* Helper constants used in defining addition *} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
13 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
14 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
15 |
xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
16 |
where |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
17 |
"xor3 a b c = (a = (b = c))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
18 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
19 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
20 |
carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
21 |
where |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
22 |
"carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
23 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
24 |
lemma carry_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
25 |
"carry True a b = (a \<or> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
26 |
"carry a True b = (a \<or> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
27 |
"carry a b True = (a \<or> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
28 |
"carry False a b = (a \<and> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
29 |
"carry a False b = (a \<and> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
30 |
"carry a b False = (a \<and> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
31 |
by (auto simp add: carry_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
32 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
33 |
lemma xor3_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
34 |
"xor3 True a b = (a = b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
35 |
"xor3 a True b = (a = b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
36 |
"xor3 a b True = (a = b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
37 |
"xor3 False a b = (a \<noteq> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
38 |
"xor3 a False b = (a \<noteq> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
39 |
"xor3 a b False = (a \<noteq> b)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
40 |
by (simp_all add: xor3_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
41 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
42 |
text {* Breaking up word equalities into equalities on their |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
43 |
bit lists. Equalities are generated and manipulated in the |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
44 |
reverse order to to_bl. *} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
45 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
46 |
lemma word_eq_rbl_eq: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
47 |
"(x = y) = (rev (to_bl x) = rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
48 |
by simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
49 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
50 |
lemma rbl_word_or: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
51 |
"rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
52 |
by (simp add: map2_def zip_rev bl_word_or rev_map) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
53 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
54 |
lemma rbl_word_and: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
55 |
"rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
56 |
by (simp add: map2_def zip_rev bl_word_and rev_map) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
57 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
58 |
lemma rbl_word_xor: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
59 |
"rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
60 |
by (simp add: map2_def zip_rev bl_word_xor rev_map) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
61 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
62 |
lemma rbl_word_not: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
63 |
"rev (to_bl (NOT x)) = map Not (rev (to_bl x))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
64 |
by (simp add: bl_word_not rev_map) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
65 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
66 |
lemma bl_word_sub: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
67 |
"to_bl (x - y) = to_bl (x + (- y))" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
51717
diff
changeset
|
68 |
by simp |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
69 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
70 |
lemma rbl_word_1: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
71 |
"rev (to_bl (1 :: ('a :: len0) word)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
72 |
= takefill False (len_of TYPE('a)) [True]" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
73 |
apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
74 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
75 |
apply (simp only: rtb_rbl_ariths(1)[OF refl]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
76 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
77 |
apply (case_tac "len_of TYPE('a)") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
78 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
79 |
apply (simp add: takefill_alt) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
80 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
81 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
82 |
lemma rbl_word_if: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
83 |
"rev (to_bl (if P then x else y)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
84 |
= map2 (If P) (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
85 |
by (simp add: map2_def split_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
86 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
87 |
lemma rbl_add_carry_Cons: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
88 |
"(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
89 |
= xor3 x y car # (if carry x y car then rbl_succ else id) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
90 |
(rbl_add xs ys)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
91 |
by (simp add: carry_def xor3_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
92 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
93 |
lemma rbl_add_suc_carry_fold: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
94 |
"length xs = length ys \<Longrightarrow> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
95 |
\<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
96 |
= (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
97 |
(zip xs ys) (\<lambda>_. [])) car" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
98 |
apply (erule list_induct2) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
99 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
100 |
apply (simp only: rbl_add_carry_Cons) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
101 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
102 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
103 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
104 |
lemma to_bl_plus_carry: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
105 |
"to_bl (x + y) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
106 |
= rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
107 |
(rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
108 |
using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
109 |
apply (simp add: word_add_rbl[OF refl refl]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
110 |
apply (drule_tac x=False in spec) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
111 |
apply (simp add: zip_rev) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
112 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
113 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
114 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
115 |
"rbl_plus cin xs ys = foldr |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
116 |
(\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
117 |
(zip xs ys) (\<lambda>_. []) cin" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
118 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
119 |
lemma rbl_plus_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
120 |
"rbl_plus cin (x # xs) (y # ys) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
121 |
= xor3 x y cin # rbl_plus (carry x y cin) xs ys" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
122 |
"rbl_plus cin [] ys = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
123 |
"rbl_plus cin xs [] = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
124 |
by (simp_all add: rbl_plus_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
125 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
126 |
lemma rbl_word_plus: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
127 |
"rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
128 |
by (simp add: rbl_plus_def to_bl_plus_carry zip_rev) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
129 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
130 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
131 |
"rbl_succ2 b xs = (if b then rbl_succ xs else xs)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
132 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
133 |
lemma rbl_succ2_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
134 |
"rbl_succ2 b [] = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
135 |
"rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
136 |
by (simp_all add: rbl_succ2_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
137 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
138 |
lemma twos_complement: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
139 |
"- x = word_succ (NOT x)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
140 |
using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
141 |
by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
142 |
del: word_add_not) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
143 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
144 |
lemma rbl_word_neg: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
145 |
"rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
146 |
by (simp add: twos_complement word_succ_rbl[OF refl] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
147 |
bl_word_not rev_map rbl_succ2_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
148 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
149 |
lemma rbl_word_cat: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
150 |
"rev (to_bl (word_cat x y :: ('a :: len0) word)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
151 |
= takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
152 |
by (simp add: word_cat_bl word_rev_tf) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
153 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
154 |
lemma rbl_word_slice: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
155 |
"rev (to_bl (slice n w :: ('a :: len0) word)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
156 |
= takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
157 |
apply (simp add: slice_take word_rev_tf rev_take) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
158 |
apply (cases "n < len_of TYPE('b)", simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
159 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
160 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
161 |
lemma rbl_word_ucast: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
162 |
"rev (to_bl (ucast x :: ('a :: len0) word)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
163 |
= takefill False (len_of TYPE('a)) (rev (to_bl x))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
164 |
apply (simp add: to_bl_ucast takefill_alt) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
165 |
apply (simp add: rev_drop) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
166 |
apply (case_tac "len_of TYPE('a) < len_of TYPE('b)") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
167 |
apply simp_all |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
168 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
169 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
170 |
lemma rbl_shiftl: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
171 |
"rev (to_bl (w << n)) = takefill False (size w) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
172 |
(replicate n False @ rev (to_bl w))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
173 |
by (simp add: bl_shiftl takefill_alt word_size rev_drop) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
174 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
175 |
lemma rbl_shiftr: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
176 |
"rev (to_bl (w >> n)) = takefill False (size w) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
177 |
(drop n (rev (to_bl w)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
178 |
by (simp add: shiftr_slice rbl_word_slice word_size) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
179 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
180 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
181 |
"drop_nonempty v n xs |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
182 |
= (if n < length xs then drop n xs else [last (v # xs)])" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
183 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
184 |
lemma drop_nonempty_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
185 |
"drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
186 |
"drop_nonempty v 0 (x # xs) = (x # xs)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
187 |
"drop_nonempty v n [] = [v]" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
188 |
by (simp_all add: drop_nonempty_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
189 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
190 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
191 |
"takefill_last x n xs = takefill (last (x # xs)) n xs" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
192 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
193 |
lemma takefill_last_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
194 |
"takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
195 |
"takefill_last z 0 xs = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
196 |
"takefill_last z n [] = replicate n z" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
197 |
apply (simp_all add: takefill_last_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
198 |
apply (simp_all add: takefill_alt) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
199 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
200 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
201 |
lemma rbl_sshiftr: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
202 |
"rev (to_bl (w >>> n)) = |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
203 |
takefill_last False (size w) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
204 |
(drop_nonempty False n (rev (to_bl w)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
205 |
apply (cases "n < size w") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
206 |
apply (simp add: bl_sshiftr takefill_last_def word_size |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
207 |
takefill_alt rev_take last_rev |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
208 |
drop_nonempty_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
209 |
apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
210 |
apply (simp add: word_size takefill_last_def takefill_alt |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
211 |
last_rev word_msb_alt word_rev_tf |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
212 |
drop_nonempty_def take_Cons') |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
213 |
apply (case_tac "len_of TYPE('a)", simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
214 |
apply (rule word_eqI) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
215 |
apply (simp add: nth_sshiftr word_size test_bit_of_bl |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
216 |
msb_nth) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
217 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
218 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
219 |
lemma nth_word_of_int: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
220 |
"(word_of_int x :: ('a :: len0) word) !! n |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
221 |
= (n < len_of TYPE('a) \<and> bin_nth x n)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
222 |
apply (simp add: test_bit_bl word_size to_bl_of_bin) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
223 |
apply (subst conj_cong[OF refl], erule bin_nth_bl) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
224 |
apply (auto) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
225 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
226 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
227 |
lemma nth_scast: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
228 |
"(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
229 |
= (n < len_of TYPE('b) \<and> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
230 |
(if n < len_of TYPE('a) - 1 then x !! n |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
231 |
else x !! (len_of TYPE('a) - 1)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
232 |
by (simp add: scast_def nth_word_of_int nth_sint) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
233 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
234 |
lemma rbl_word_scast: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
235 |
"rev (to_bl (scast x :: ('a :: len) word)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
236 |
= takefill_last False (len_of TYPE('a)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
237 |
(rev (to_bl x))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
238 |
apply (rule nth_equalityI) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
239 |
apply (simp add: word_size takefill_last_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
240 |
apply (clarsimp simp: nth_scast takefill_last_def |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
241 |
nth_takefill word_size nth_rev to_bl_nth) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
242 |
apply (cases "len_of TYPE('b)") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
243 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
244 |
apply (clarsimp simp: less_Suc_eq_le linorder_not_less |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
245 |
last_rev word_msb_alt[symmetric] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
246 |
msb_nth) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
247 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
248 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
249 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
250 |
rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
251 |
where |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
252 |
"rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
253 |
xs []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
254 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
255 |
lemma rbl_mul_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
256 |
"rbl_mul (x # xs) ys |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
257 |
= rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
258 |
"rbl_mul [] ys = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
259 |
by (simp_all add: rbl_mul_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
260 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
261 |
lemma takefill_le2: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
262 |
"length xs \<le> n \<Longrightarrow> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
263 |
takefill x m (takefill x n xs) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
264 |
= takefill x m xs" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
265 |
by (simp add: takefill_alt replicate_add[symmetric]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
266 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
267 |
lemma take_rbl_plus: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
268 |
"\<forall>n b. take n (rbl_plus b xs ys) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
269 |
= rbl_plus b (take n xs) (take n ys)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
270 |
apply (simp add: rbl_plus_def take_zip[symmetric]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
271 |
apply (rule_tac list="zip xs ys" in list.induct) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
272 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
273 |
apply (clarsimp simp: split_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
274 |
apply (case_tac n, simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
275 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
276 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
277 |
lemma word_rbl_mul_induct: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
278 |
fixes y :: "'a :: len word" shows |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
279 |
"length xs \<le> size y |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
280 |
\<Longrightarrow> rbl_mul xs (rev (to_bl y)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
281 |
= take (length xs) (rev (to_bl (of_bl (rev xs) * y)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
282 |
proof (induct xs) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
283 |
case Nil |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
284 |
show ?case |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
285 |
by (simp add: rbl_mul_simps) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
286 |
next |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
287 |
case (Cons z zs) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
288 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
289 |
have rbl_word_plus': |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
290 |
"\<And>(x :: 'a word) y. |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
291 |
to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
292 |
by (simp add: rbl_word_plus[symmetric]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
293 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
294 |
have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
295 |
apply (cases z) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
296 |
apply (simp cong: map_cong) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
297 |
apply (simp add: map_replicate_const cong: map_cong) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
298 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
299 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
300 |
have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
301 |
by (simp add: shiftl_t2n) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
302 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
303 |
have zip_take_triv: "\<And>xs ys n. n = length ys |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
304 |
\<Longrightarrow> zip (take n xs) ys = zip xs ys" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
305 |
by (rule nth_equalityI, simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
306 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
307 |
show ?case |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
308 |
using Cons |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
309 |
apply (simp add: trans [OF of_bl_append add_commute] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
310 |
rbl_mul_simps rbl_word_plus' |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47567
diff
changeset
|
311 |
Cons.hyps distrib_right mult_bit |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
312 |
shiftl rbl_shiftl) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
313 |
apply (simp add: takefill_alt word_size rev_map take_rbl_plus |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
314 |
min_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
315 |
apply (simp add: rbl_plus_def zip_take_triv) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
316 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
317 |
qed |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
318 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
319 |
lemma rbl_word_mul: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
320 |
fixes x :: "'a :: len word" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
321 |
shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
322 |
using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
323 |
by (simp add: word_size) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
324 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
325 |
text {* Breaking up inequalities into bitlist properties. *} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
326 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
327 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
328 |
"rev_bl_order F xs ys = |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
329 |
(length xs = length ys \<and> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
330 |
((xs = ys \<and> F) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
331 |
\<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
332 |
\<and> \<not> xs ! n \<and> ys ! n)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
333 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
334 |
lemma rev_bl_order_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
335 |
"rev_bl_order F [] [] = F" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
336 |
"rev_bl_order F (x # xs) (y # ys) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
337 |
= rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
338 |
apply (simp_all add: rev_bl_order_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
339 |
apply (rule conj_cong[OF refl]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
340 |
apply (cases "xs = ys") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
341 |
apply (simp add: nth_Cons') |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
342 |
apply blast |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
343 |
apply (simp add: nth_Cons') |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
344 |
apply safe |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
345 |
apply (rule_tac x="n - 1" in exI) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
346 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
347 |
apply (rule_tac x="Suc n" in exI) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
348 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
349 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
350 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
351 |
lemma rev_bl_order_rev_simp: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
352 |
"length xs = length ys \<Longrightarrow> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
353 |
rev_bl_order F (xs @ [x]) (ys @ [y]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
354 |
= ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
355 |
apply (induct arbitrary: F rule: list_induct2) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
356 |
apply (auto simp add: rev_bl_order_simps) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
357 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
358 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
359 |
lemma rev_bl_order_bl_to_bin: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
360 |
"length xs = length ys |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
361 |
\<Longrightarrow> rev_bl_order True xs ys |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
362 |
= (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
363 |
\<and> rev_bl_order False xs ys |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
364 |
= (bl_to_bin (rev xs) < bl_to_bin (rev ys))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
365 |
apply (induct xs ys rule: list_induct2) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
366 |
apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
367 |
apply (simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
368 |
apply arith? |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
369 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
370 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
371 |
lemma word_le_rbl: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
372 |
fixes x :: "('a :: len0) word" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
373 |
shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
374 |
by (simp add: rev_bl_order_bl_to_bin word_le_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
375 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
376 |
lemma word_less_rbl: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
377 |
fixes x :: "('a :: len0) word" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
378 |
shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
379 |
by (simp add: word_less_alt rev_bl_order_bl_to_bin) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
380 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
381 |
lemma word_sint_msb_eq: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
382 |
"sint x = uint x - (if msb x then 2 ^ size x else 0)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
383 |
apply (cases "msb x") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
384 |
apply (rule word_sint.Abs_eqD[where 'a='a], simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
385 |
apply (simp add: word_size wi_hom_syms |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
386 |
word_of_int_2p_len) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
387 |
apply (simp add: sints_num word_size) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
388 |
apply (rule conjI) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
389 |
apply (simp add: le_diff_eq') |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
390 |
apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
391 |
apply (simp add: power_Suc[symmetric]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
392 |
apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
393 |
apply (rule notI, drule word_eqD[where x="size x - 1"]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
394 |
apply (simp add: msb_nth word_ops_nth_size word_size) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
395 |
apply (simp add: order_less_le_trans[where y=0]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
396 |
apply (rule word_uint.Abs_eqD[where 'a='a], simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
397 |
apply (simp add: linorder_not_less uints_num word_msb_sint) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
398 |
apply (rule order_less_le_trans[OF sint_lt]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
399 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
400 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
401 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
402 |
lemma word_sle_msb_le: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
403 |
"(x <=s y) = ((msb y --> msb x) \<and> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
404 |
((msb x \<and> \<not> msb y) \<or> (x <= y)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
405 |
apply (simp add: word_sle_def word_sint_msb_eq word_size |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
406 |
word_le_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
407 |
apply safe |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
408 |
apply (rule order_trans[OF _ uint_ge_0]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
409 |
apply (simp add: order_less_imp_le) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
410 |
apply (erule notE[OF leD]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
411 |
apply (rule order_less_le_trans[OF _ uint_ge_0]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
412 |
apply simp |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
413 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
414 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
415 |
lemma word_sless_msb_less: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
416 |
"(x <s y) = ((msb y --> msb x) \<and> |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
417 |
((msb x \<and> \<not> msb y) \<or> (x < y)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
418 |
by (auto simp add: word_sless_def word_sle_msb_le) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
419 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
420 |
definition |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
421 |
"map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
422 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
423 |
lemma map_last_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
424 |
"map_last f [] = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
425 |
"map_last f [x] = [f x]" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
426 |
"map_last f (x # y # zs) = x # map_last f (y # zs)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
427 |
by (simp_all add: map_last_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
428 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
429 |
lemma word_sle_rbl: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
430 |
"(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x))) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
431 |
(map_last Not (rev (to_bl y)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
432 |
using word_msb_alt[where w=x] word_msb_alt[where w=y] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
433 |
apply (simp add: word_sle_msb_le word_le_rbl) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
434 |
apply (subgoal_tac "length (to_bl x) = length (to_bl y)") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
435 |
apply (cases "to_bl x", simp) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
436 |
apply (cases "to_bl y", simp) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
437 |
apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
438 |
apply auto |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
439 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
440 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
441 |
lemma word_sless_rbl: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
442 |
"(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x))) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
443 |
(map_last Not (rev (to_bl y)))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
444 |
using word_msb_alt[where w=x] word_msb_alt[where w=y] |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
445 |
apply (simp add: word_sless_msb_less word_less_rbl) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
446 |
apply (subgoal_tac "length (to_bl x) = length (to_bl y)") |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
447 |
apply (cases "to_bl x", simp) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
448 |
apply (cases "to_bl y", simp) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
449 |
apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
450 |
apply auto |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
451 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
452 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
453 |
text {* Lemmas for unpacking rev (to_bl n) for numerals n and also |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
454 |
for irreducible values and expressions. *} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
455 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
456 |
lemma rev_bin_to_bl_simps: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
457 |
"rev (bin_to_bl 0 x) = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
458 |
"rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
459 |
= False # rev (bin_to_bl n (numeral nm))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
460 |
"rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
461 |
= True # rev (bin_to_bl n (numeral nm))" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
462 |
"rev (bin_to_bl (Suc n) (numeral (num.One))) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
463 |
= True # replicate n False" |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
464 |
"rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
465 |
= False # rev (bin_to_bl n (- numeral nm))" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
466 |
"rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
467 |
= True # rev (bin_to_bl n (- numeral (nm + num.One)))" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
468 |
"rev (bin_to_bl (Suc n) (- numeral (num.One))) |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
469 |
= True # replicate n True" |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
470 |
"rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
471 |
= True # rev (bin_to_bl n (- numeral (nm + num.One)))" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
472 |
"rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
473 |
= False # rev (bin_to_bl n (- numeral (nm + num.One)))" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
474 |
"rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
475 |
= False # rev (bin_to_bl n (- numeral num.One))" |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
476 |
apply (simp_all add: bin_to_bl_def) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
477 |
apply (simp_all only: bin_to_bl_aux_alt) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
478 |
apply (simp_all) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
479 |
apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
480 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
481 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
482 |
lemma to_bl_upt: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
483 |
"to_bl x = rev (map (op !! x) [0 ..< size x])" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
484 |
apply (rule nth_equalityI) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
485 |
apply (simp add: word_size) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
486 |
apply (clarsimp simp: to_bl_nth word_size nth_rev) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
487 |
done |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
488 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
489 |
lemma rev_to_bl_upt: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
490 |
"rev (to_bl x) = map (op !! x) [0 ..< size x]" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
491 |
by (simp add: to_bl_upt) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
492 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
493 |
lemma upt_eq_list_intros: |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
494 |
"j <= i \<Longrightarrow> [i ..< j] = []" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
495 |
"\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
496 |
by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
497 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
498 |
text {* Tactic definition *} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
499 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
500 |
ML {* |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
501 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
502 |
structure Word_Bitwise_Tac = struct |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
503 |
|
51686 | 504 |
val word_ss = simpset_of @{theory_context Word}; |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
505 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
506 |
fun mk_nat_clist ns = List.foldr |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
507 |
(uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"})) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
508 |
@{cterm "[] :: nat list"} ns; |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
509 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
510 |
fun upt_conv ctxt ct = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
511 |
case term_of ct of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
512 |
(@{const upt} $ n $ m) => |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
513 |
let |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
514 |
val (i, j) = pairself (snd o HOLogic.dest_number) (n, m); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
515 |
val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1)) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
516 |
|> mk_nat_clist; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
517 |
val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
518 |
|> Thm.apply @{cterm Trueprop}; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
519 |
in |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
520 |
try (fn () => |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
521 |
Goal.prove_internal [] prop |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
522 |
(K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1 |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
523 |
ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) () |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
524 |
end |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
525 |
| _ => NONE; |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
526 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
527 |
val expand_upt_simproc = Simplifier.make_simproc |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
528 |
{lhss = [@{cpat "upt _ _"}], |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
529 |
name = "expand_upt", identifier = [], |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
530 |
proc = K upt_conv}; |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
531 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
532 |
fun word_len_simproc_fn ctxt ct = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
533 |
case term_of ct of |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
534 |
Const (@{const_name len_of}, _) $ t => (let |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
535 |
val T = fastype_of t |> dest_Type |> snd |> the_single |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
536 |
val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T); |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
537 |
val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
538 |
|> Thm.apply @{cterm Trueprop}; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
539 |
in Goal.prove_internal [] prop (K (simp_tac (put_simpset word_ss ctxt) 1)) |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
540 |
|> mk_meta_eq |> SOME end |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
541 |
handle TERM _ => NONE | TYPE _ => NONE) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
542 |
| _ => NONE; |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
543 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
544 |
val word_len_simproc = Simplifier.make_simproc |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
545 |
{lhss = [@{cpat "len_of _"}], |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
546 |
name = "word_len", identifier = [], |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
547 |
proc = K word_len_simproc_fn}; |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
548 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
549 |
(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2, |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
550 |
or just 5 (discarding nat) when n_sucs = 0 *) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
551 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
552 |
fun nat_get_Suc_simproc_fn n_sucs ctxt ct = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
553 |
let |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
554 |
val thy = Proof_Context.theory_of ctxt; |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
555 |
val (f $ arg) = (term_of ct); |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
556 |
val n = (case arg of @{term nat} $ n => n | n => n) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
557 |
|> HOLogic.dest_number |> snd; |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
558 |
val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
559 |
else (n, 0); |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
560 |
val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
561 |
(replicate i @{term Suc}); |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
562 |
val _ = if arg = arg' then raise TERM ("", []) else (); |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
563 |
fun propfn g = HOLogic.mk_eq (g arg, g arg') |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
564 |
|> HOLogic.mk_Trueprop |> cterm_of thy; |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
565 |
val eq1 = Goal.prove_internal [] (propfn I) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
566 |
(K (simp_tac (put_simpset word_ss ctxt) 1)); |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
567 |
in Goal.prove_internal [] (propfn (curry (op $) f)) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
568 |
(K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1)) |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
569 |
|> mk_meta_eq |> SOME end |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
570 |
handle TERM _ => NONE; |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
571 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
572 |
fun nat_get_Suc_simproc n_sucs thy cts = Simplifier.make_simproc |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
573 |
{lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts, |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
574 |
name = "nat_get_Suc", identifier = [], |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
575 |
proc = K (nat_get_Suc_simproc_fn n_sucs)}; |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
576 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
577 |
val no_split_ss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
578 |
simpset_of (put_simpset HOL_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
579 |
|> Splitter.del_split @{thm split_if}); |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
580 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
581 |
val expand_word_eq_sss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
582 |
(simpset_of (put_simpset HOL_basic_ss @{context} addsimps |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
583 |
@{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
584 |
map simpset_of [ |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
585 |
put_simpset no_split_ss @{context} addsimps |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
586 |
@{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
587 |
rbl_word_neg bl_word_sub rbl_word_xor |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
588 |
rbl_word_cat rbl_word_slice rbl_word_scast |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
589 |
rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
590 |
rbl_word_if}, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
591 |
put_simpset no_split_ss @{context} addsimps |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
592 |
@{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1}, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
593 |
put_simpset no_split_ss @{context} addsimps |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
594 |
@{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size} |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
595 |
addsimprocs [word_len_simproc], |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
596 |
put_simpset no_split_ss @{context} addsimps |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
597 |
@{thms list.simps split_conv replicate.simps map.simps |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
598 |
zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
599 |
foldr.simps map2_Cons map2_Nil takefill_Suc_Cons |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
600 |
takefill_Suc_Nil takefill.Z rbl_succ2_simps |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
601 |
rbl_plus_simps rev_bin_to_bl_simps append.simps |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
602 |
takefill_last_simps drop_nonempty_simps |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
603 |
rev_bl_order_simps} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
604 |
addsimprocs [expand_upt_simproc, |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
605 |
nat_get_Suc_simproc 4 @{theory} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
606 |
[@{cpat replicate}, @{cpat "takefill ?x"}, |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
607 |
@{cpat drop}, @{cpat "bin_to_bl"}, |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
608 |
@{cpat "takefill_last ?x"}, |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
609 |
@{cpat "drop_nonempty ?x"}]], |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
610 |
put_simpset no_split_ss @{context} addsimps @{thms xor3_simps carry_simps if_bool_simps} |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
611 |
]) |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
612 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
613 |
fun tac ctxt = |
50107 | 614 |
let |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
615 |
val (ss, sss) = expand_word_eq_sss; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
616 |
in |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
617 |
foldr1 (op THEN_ALL_NEW) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
618 |
((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) :: |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
619 |
map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
620 |
end; |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
621 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
622 |
end |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
623 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
624 |
*} |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
625 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
626 |
method_setup word_bitwise = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
627 |
{* Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1)) *} |
47567
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
628 |
"decomposer for word equalities and inequalities into bit propositions" |
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
629 |
|
407cabf66f21
New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
diff
changeset
|
630 |
end |