Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
b98ab16c
Commit
b98ab16c
authored
Jan 29, 2016
by
Stefan Berghofer
Browse files
Adapted Isabelle realization to changes in bv.why
parent
cbe8fa3d
Changes
2
Hide whitespace changes
Inline
Side-by-side
lib/isabelle/Why3_BV.thy.2015
View file @
b98ab16c
...
...
@@ -248,7 +248,7 @@ type_synonym word8 = "8 word"
why3_open "bv/BV8.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -285,7 +285,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -316,7 +316,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -328,7 +328,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -338,7 +338,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -362,7 +362,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
@@ -444,7 +444,7 @@ type_synonym word16 = "16 word"
why3_open "bv/BV16.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -481,7 +481,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -512,7 +512,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -524,7 +524,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -534,7 +534,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -558,7 +558,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
@@ -640,7 +640,7 @@ type_synonym word32 = "32 word"
why3_open "bv/BV32.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -677,7 +677,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -708,7 +708,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -720,7 +720,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -730,7 +730,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -754,7 +754,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
@@ -836,7 +836,7 @@ type_synonym word64 = "64 word"
why3_open "bv/BV64.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -873,7 +873,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -904,7 +904,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -916,7 +916,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -926,7 +926,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -950,7 +950,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
lib/isabelle/Why3_BV.thy.2016
View file @
b98ab16c
...
...
@@ -248,7 +248,7 @@ type_synonym word8 = "8 word"
why3_open "bv/BV8.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -285,7 +285,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -316,7 +316,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -328,7 +328,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -338,7 +338,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -362,7 +362,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
@@ -444,7 +444,7 @@ type_synonym word16 = "16 word"
why3_open "bv/BV16.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -481,7 +481,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -512,7 +512,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -524,7 +524,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -534,7 +534,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -558,7 +558,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
@@ -640,7 +640,7 @@ type_synonym word32 = "32 word"
why3_open "bv/BV32.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -677,7 +677,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -708,7 +708,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -720,7 +720,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -730,7 +730,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -754,7 +754,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
@@ -836,7 +836,7 @@ type_synonym word64 = "64 word"
why3_open "bv/BV64.xml"
constants
zero=zero_class.zero
zero
s
=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
...
...
@@ -873,7 +873,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zero
s
by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
...
...
@@ -904,7 +904,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zero
s
by simp
why3_vc Asr_nth_low
using assms
...
...
@@ -916,7 +916,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zero
s
by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
...
...
@@ -926,7 +926,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zero
s
by simp
why3_vc to_uint_extensionality using assms by simp
...
...
@@ -950,7 +950,7 @@ why3_vc Nth_bv_is_nth2
using assms
by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
why3_vc Of_int_zero by simp
why3_vc Of_int_zero
s
by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment