From e2289d8a86ff57881e1008b42a11409974254b69 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 11 Jul 2018 13:22:18 +0100 Subject: Update Isabelle and HOL snapshots --- .../lib/hol/sail2_operators_bitlistsScript.sml | 36 +++++++++++----------- .../sail/lib/hol/sail2_operators_mwordsScript.sml | 36 +++++++++++----------- .../isabelle/lib/sail/Sail2_operators_bitlists.thy | 36 +++++++++++----------- .../isabelle/lib/sail/Sail2_operators_mwords.thy | 36 +++++++++++----------- .../lib/sail/Sail2_operators_mwords_lemmas.thy | 9 +++--- 5 files changed, 76 insertions(+), 77 deletions(-) (limited to 'snapshots') diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml index da349336..88c06749 100644 --- a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml +++ b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml @@ -328,42 +328,42 @@ val _ = Define ` instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T))`; -(*val add_vec_int : list bitU -> integer -> list bitU*) -(*val sub_vec_int : list bitU -> integer -> list bitU*) -(*val mult_vec_int : list bitU -> integer -> list bitU*) +(*val add_vec_int : list bitU -> integer -> list bitU*) +(*val sub_vec_int : list bitU -> integer -> list bitU*) +(*val mult_vec_int : list bitU -> integer -> list bitU*) val _ = Define ` - ((add_vec_int0:(bitU)list -> int ->(bitU)list) l r= (arith_op_bv_int + ((add_vec_int0:(bitU)list -> int ->(bitU)list) l r= (arith_op_bv_int (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`; + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`; val _ = Define ` - ((sub_vec_int0:(bitU)list -> int ->(bitU)list) l r= (arith_op_bv_int + ((sub_vec_int0:(bitU)list -> int ->(bitU)list) l r= (arith_op_bv_int (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`; + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`; val _ = Define ` - ((mult_vec_int0:(bitU)list -> int ->(bitU)list) l r= (arith_op_double_bl + ((mult_vec_int0:(bitU)list -> int ->(bitU)list) l r= (arith_op_double_bl (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`; + instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`; -(*val add_int_vec : integer -> list bitU -> list bitU*) -(*val sub_int_vec : integer -> list bitU -> list bitU*) -(*val mult_int_vec : integer -> list bitU -> list bitU*) +(*val add_int_vec : integer -> list bitU -> list bitU*) +(*val sub_int_vec : integer -> list bitU -> list bitU*) +(*val mult_int_vec : integer -> list bitU -> list bitU*) val _ = Define ` - ((add_int_vec0:int ->(bitU)list ->(bitU)list) l r= (arith_op_int_bv + ((add_int_vec0:int ->(bitU)list ->(bitU)list) l r= (arith_op_int_bv (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`; + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`; val _ = Define ` - ((sub_int_vec0:int ->(bitU)list ->(bitU)list) l r= (arith_op_int_bv + ((sub_int_vec0:int ->(bitU)list ->(bitU)list) l r= (arith_op_int_bv (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`; + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`; val _ = Define ` - ((mult_int_vec0:int ->(bitU)list ->(bitU)list) l r= (arith_op_double_bl + ((mult_int_vec0:int ->(bitU)list ->(bitU)list) l r= (arith_op_double_bl (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`; + instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`; (*val add_vec_bit : list bitU -> bitU -> list bitU*) diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml index 9276cfef..5b0e7723 100644 --- a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml +++ b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml @@ -278,36 +278,36 @@ val _ = Define ` ((mults_vec:'a words$word -> 'a words$word -> 'b words$word) l r= (integer_word$i2w ((int_of_mword T (words$sw2sw l : 'b words$word)) * (int_of_mword T (words$sw2sw r : 'b words$word)))))`; -(*val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) -(*val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) -(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*) +(*val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) +(*val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) +(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*) val _ = Define ` - ((add_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int - instance_Sail2_values_Bitvector_Machine_word_mword_dict (+) T l r))`; + ((add_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int + instance_Sail2_values_Bitvector_Machine_word_mword_dict (+) F l r))`; val _ = Define ` - ((sub_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int - instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) T l r))`; + ((sub_vec_int:'a words$word -> int -> 'a words$word) l r= (arith_op_bv_int + instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) F l r))`; val _ = Define ` - ((mult_vec_int:'a words$word -> int -> 'b words$word) l r= (arith_op_bv_int - instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * ) T (words$sw2sw l : 'b words$word) r))`; + ((mult_vec_int:'a words$word -> int -> 'b words$word) l r= (arith_op_bv_int + instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * ) F (words$w2w l : 'b words$word) r))`; -(*val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) -(*val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) -(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*) +(*val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) +(*val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) +(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*) val _ = Define ` - ((add_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv - instance_Sail2_values_Bitvector_Machine_word_mword_dict (+) T l r))`; + ((add_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv + instance_Sail2_values_Bitvector_Machine_word_mword_dict (+) F l r))`; val _ = Define ` - ((sub_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv - instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) T l r))`; + ((sub_int_vec:int -> 'a words$word -> 'a words$word) l r= (arith_op_int_bv + instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) F l r))`; val _ = Define ` - ((mult_int_vec:int -> 'a words$word -> 'b words$word) l r= (arith_op_int_bv - instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * ) T l (words$sw2sw r : 'b words$word)))`; + ((mult_int_vec:int -> 'a words$word -> 'b words$word) l r= (arith_op_int_bv + instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * ) F l (words$w2w r : 'b words$word)))`; (*val add_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a*) diff --git a/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy b/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy index 96c38a6a..35f43769 100644 --- a/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy +++ b/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy @@ -333,42 +333,42 @@ definition mults_vec :: "(bitU)list \(bitU)list \(bitU) instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) True )" -(*val add_vec_int : list bitU -> integer -> list bitU*) -(*val sub_vec_int : list bitU -> integer -> list bitU*) -(*val mult_vec_int : list bitU -> integer -> list bitU*) +(*val add_vec_int : list bitU -> integer -> list bitU*) +(*val sub_vec_int : list bitU -> integer -> list bitU*) +(*val mult_vec_int : list bitU -> integer -> list bitU*) definition add_vec_int :: "(bitU)list \ int \(bitU)list " where - " add_vec_int l r = ( arith_op_bv_int + " add_vec_int l r = ( arith_op_bv_int (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) True l r )" + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) False l r )" definition sub_vec_int :: "(bitU)list \ int \(bitU)list " where - " sub_vec_int l r = ( arith_op_bv_int + " sub_vec_int l r = ( arith_op_bv_int (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) True l r )" + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) False l r )" definition mult_vec_int :: "(bitU)list \ int \(bitU)list " where - " mult_vec_int l r = ( arith_op_double_bl + " mult_vec_int l r = ( arith_op_double_bl (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) True l (List.map (\ b. b) (bits_of_int (int (List.length l)) r)))" + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) False l (List.map (\ b. b) (bits_of_int (int (List.length l)) r)))" -(*val add_int_vec : integer -> list bitU -> list bitU*) -(*val sub_int_vec : integer -> list bitU -> list bitU*) -(*val mult_int_vec : integer -> list bitU -> list bitU*) +(*val add_int_vec : integer -> list bitU -> list bitU*) +(*val sub_int_vec : integer -> list bitU -> list bitU*) +(*val mult_int_vec : integer -> list bitU -> list bitU*) definition add_int_vec :: " int \(bitU)list \(bitU)list " where - " add_int_vec l r = ( arith_op_int_bv + " add_int_vec l r = ( arith_op_int_bv (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) True l r )" + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) False l r )" definition sub_int_vec :: " int \(bitU)list \(bitU)list " where - " sub_int_vec l r = ( arith_op_int_bv + " sub_int_vec l r = ( arith_op_int_bv (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) True l r )" + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) False l r )" definition mult_int_vec :: " int \(bitU)list \(bitU)list " where - " mult_int_vec l r = ( arith_op_double_bl + " mult_int_vec l r = ( arith_op_double_bl (instance_Sail2_values_Bitvector_list_dict - instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) True (List.map (\ b. b) (bits_of_int (int (List.length r)) l)) r )" + instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) False (List.map (\ b. b) (bits_of_int (int (List.length r)) l)) r )" (*val add_vec_bit : list bitU -> bitU -> list bitU*) diff --git a/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy b/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy index c6d1a865..44d29a7f 100644 --- a/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy +++ b/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy @@ -283,36 +283,36 @@ definition mults_vec :: "('a::len)Word.word \('a::len)Word.word \ mword 'a -> integer -> mword 'a*) -(*val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) -(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*) +(*val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) +(*val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*) +(*val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b*) definition add_vec_int :: "('a::len)Word.word \ int \('a::len)Word.word " where - " add_vec_int l r = ( arith_op_bv_int - instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+) True l r )" + " add_vec_int l r = ( arith_op_bv_int + instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+) False l r )" definition sub_vec_int :: "('a::len)Word.word \ int \('a::len)Word.word " where - " sub_vec_int l r = ( arith_op_bv_int - instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) True l r )" + " sub_vec_int l r = ( arith_op_bv_int + instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) False l r )" definition mult_vec_int :: "('a::len)Word.word \ int \('b::len)Word.word " where - " mult_vec_int l r = ( arith_op_bv_int - instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*) True (Word.scast l :: ( 'b::len)Word.word) r )" + " mult_vec_int l r = ( arith_op_bv_int + instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*) False (Word.ucast l :: ( 'b::len)Word.word) r )" -(*val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) -(*val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) -(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*) +(*val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) +(*val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a*) +(*val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*) definition add_int_vec :: " int \('a::len)Word.word \('a::len)Word.word " where - " add_int_vec l r = ( arith_op_int_bv - instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+) True l r )" + " add_int_vec l r = ( arith_op_int_bv + instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+) False l r )" definition sub_int_vec :: " int \('a::len)Word.word \('a::len)Word.word " where - " sub_int_vec l r = ( arith_op_int_bv - instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) True l r )" + " sub_int_vec l r = ( arith_op_int_bv + instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) False l r )" definition mult_int_vec :: " int \('a::len)Word.word \('b::len)Word.word " where - " mult_int_vec l r = ( arith_op_int_bv - instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*) True l (Word.scast r :: ( 'b::len)Word.word))" + " mult_int_vec l r = ( arith_op_int_bv + instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*) False l (Word.ucast r :: ( 'b::len)Word.word))" (*val add_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a*) diff --git a/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy b/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy index 47bf32b2..fd54c93a 100644 --- a/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy +++ b/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy @@ -153,11 +153,10 @@ declare adds_vec_def[simp] declare subs_vec_def[simp] declare mults_vec_def[simp] -lemma arith_vec_int_simps: - fixes l :: "'a::len word" - shows "add_vec_int l r = word_of_int (sint l + sint (word_of_int r :: 'a word))" - and "sub_vec_int l r = word_of_int (sint l - sint (word_of_int r :: 'a word))" - and "(mult_vec_int l r :: 'b::len word) = word_of_int (sint (scast l :: 'b word) * sint (word_of_int r :: 'b word))" +lemma arith_vec_int_simps[simp]: + "add_vec_int l r = l + (word_of_int r)" + "sub_vec_int l r = l - (word_of_int r)" + "mult_vec_int l r = (ucast l) * (word_of_int r)" unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) -- cgit v1.2.3