Commit e2b5e272 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Isabelle realizations: update for removed axioms from BV theories

parent 701397eb
...@@ -279,8 +279,6 @@ why3_open "bv/BV8.xml" ...@@ -279,8 +279,6 @@ why3_open "bv/BV8.xml"
types types
t=word8 t=word8
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -423,10 +421,6 @@ why3_vc to_uint_lsl ...@@ -423,10 +421,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
...@@ -475,8 +469,6 @@ why3_open "bv/BV16.xml" ...@@ -475,8 +469,6 @@ why3_open "bv/BV16.xml"
types types
t=word16 t=word16
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -619,10 +611,6 @@ why3_vc to_uint_lsl ...@@ -619,10 +611,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
...@@ -671,8 +659,6 @@ why3_open "bv/BV32.xml" ...@@ -671,8 +659,6 @@ why3_open "bv/BV32.xml"
types types
t=word32 t=word32
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -815,10 +801,6 @@ why3_vc to_uint_lsl ...@@ -815,10 +801,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
...@@ -867,8 +849,6 @@ why3_open "bv/BV64.xml" ...@@ -867,8 +849,6 @@ why3_open "bv/BV64.xml"
types types
t=word64 t=word64
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -1011,10 +991,6 @@ why3_vc to_uint_lsl ...@@ -1011,10 +991,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
......
...@@ -279,8 +279,6 @@ why3_open "bv/BV8.xml" ...@@ -279,8 +279,6 @@ why3_open "bv/BV8.xml"
types types
t=word8 t=word8
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -423,10 +421,6 @@ why3_vc to_uint_lsl ...@@ -423,10 +421,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
...@@ -475,8 +469,6 @@ why3_open "bv/BV16.xml" ...@@ -475,8 +469,6 @@ why3_open "bv/BV16.xml"
types types
t=word16 t=word16
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -619,10 +611,6 @@ why3_vc to_uint_lsl ...@@ -619,10 +611,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
...@@ -671,8 +659,6 @@ why3_open "bv/BV32.xml" ...@@ -671,8 +659,6 @@ why3_open "bv/BV32.xml"
types types
t=word32 t=word32
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -815,10 +801,6 @@ why3_vc to_uint_lsl ...@@ -815,10 +801,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
...@@ -867,8 +849,6 @@ why3_open "bv/BV64.xml" ...@@ -867,8 +849,6 @@ why3_open "bv/BV64.xml"
types types
t=word64 t=word64
why3_vc size_pos by simp
why3_vc nth_out_of_bound why3_vc nth_out_of_bound
using assms using assms
by (auto simp add: bv_nth_def test_bit_bin) by (auto simp add: bv_nth_def test_bit_bin)
...@@ -1011,10 +991,6 @@ why3_vc to_uint_lsl ...@@ -1011,10 +991,6 @@ why3_vc to_uint_lsl
by (simp add: emod_def shiftl_t2n unat_def by (simp add: emod_def shiftl_t2n unat_def
uint_word_ariths mult_ac uint_pow pull_mods) uint_word_ariths mult_ac uint_pow pull_mods)
why3_vc two_power_size_val by simp
why3_vc max_int_val by simp
why3_vc Extensionality why3_vc Extensionality
using assms using assms
by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat) by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment