diff --git a/thys/Dict_Construction/dict_construction_util.ML b/thys/Dict_Construction/dict_construction_util.ML --- a/thys/Dict_Construction/dict_construction_util.ML +++ b/thys/Dict_Construction/dict_construction_util.ML @@ -1,316 +1,316 @@ infixr 5 ==> infixr ===> infix 1 CONTINUE_WITH CONTINUE_WITH_FW signature DICT_CONSTRUCTION_UTIL = sig (* general *) val split_list3: ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val symreltab_of_symtab: 'a Symtab.table Symtab.table -> 'a Symreltab.table val zip_symtabs: ('a -> 'b -> 'c) -> 'a Symtab.table -> 'b Symtab.table -> 'c Symtab.table val cat_options: 'a option list -> 'a list val partition: ('a -> bool) -> 'a list -> 'a list * 'a list val unappend: 'a list * 'b -> 'c list -> 'c list * 'c list val flat_right: ('a * 'b list) list -> ('a * 'b) list (* logic *) val ===> : term list * term -> term val ==> : term * term -> term val sortify: sort -> term -> term val sortify_typ: sort -> typ -> typ val typify: term -> term val typify_typ: typ -> typ val all_frees: term -> (string * typ) list val all_frees': term -> string list val all_tfrees: typ -> (string * sort) list (* printing *) val pretty_const: Proof.context -> string -> Pretty.T (* conversion/tactic *) val ANY: tactic list -> tactic val ANY': ('a -> tactic) list -> 'a -> tactic val CONTINUE_WITH: (int -> tactic) * (int -> tactic) list -> int -> thm -> thm Seq.seq val CONTINUE_WITH_FW: (int -> tactic) * (int -> tactic) list -> int -> thm -> thm Seq.seq val SOLVED: tactic -> tactic val TRY': ('a -> tactic) -> 'a -> tactic val descend_fun_conv: conv -> conv val lhs_conv: conv -> conv val rhs_conv: conv -> conv val rewr_lhs_head_conv: thm -> conv val rewr_rhs_head_conv: thm -> conv val conv_result: ('a -> thm) -> 'a -> term val changed_conv: ('a -> thm) -> 'a -> thm val maybe_induct_tac: thm list option -> term list list -> term list list -> Proof.context -> tactic val multi_induct_tac: thm list -> term list list -> term list list -> Proof.context -> tactic val print_tac': Proof.context -> string -> int -> tactic val fo_cong_tac: Proof.context -> thm -> int -> tactic (* theorem manipulation *) val contract: Proof.context -> thm -> thm val on_thms_complete: (unit -> 'a) -> thm list -> thm list (* theory *) val define_params_nosyn: term -> local_theory -> thm * local_theory val note_thm: binding -> thm -> local_theory -> thm * local_theory val note_thms: binding -> thm list -> local_theory -> thm list * local_theory (* timing *) val with_timeout: Time.time -> ('a -> 'a) -> 'a -> 'a (* debugging *) val debug: bool Config.T val if_debug: Proof.context -> (unit -> unit) -> unit val ALLGOALS': Proof.context -> (int -> tactic) -> tactic val prove': Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_common': Proof.context -> string list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> thm list end structure Dict_Construction_Util : DICT_CONSTRUCTION_UTIL = struct (* general *) fun symreltab_of_symtab tab = Symtab.map (K Symtab.dest) tab |> Symtab.dest |> maps (fn (k, kvs) => map (apfst (pair k)) kvs) |> Symreltab.make fun split_list3 [] = ([], [], []) | split_list3 ((x, y, z) :: rest) = let val (xs, ys, zs) = split_list3 rest in (x :: xs, y :: ys, z :: zs) end fun zip_symtabs f t1 t2 = let open Symtab val ord = fast_string_ord fun aux acc [] [] = acc | aux acc ((k1, x) :: xs) ((k2, y) :: ys) = (case ord (k1, k2) of EQUAL => aux (update_new (k1, f x y) acc) xs ys | LESS => raise UNDEF k1 | GREATER => raise UNDEF k2) | aux _ ((k, _) :: _) [] = raise UNDEF k | aux _ [] ((k, _) :: _) = raise UNDEF k in aux empty (dest t1) (dest t2) end fun cat_options [] = [] | cat_options (SOME x :: xs) = x :: cat_options xs | cat_options (NONE :: xs) = cat_options xs fun partition f xs = (filter f xs, filter_out f xs) fun unappend (xs, _) = chop (length xs) fun flat_right [] = [] | flat_right ((x, ys) :: rest) = map (pair x) ys @ flat_right rest (* logic *) fun x ==> y = Logic.mk_implies (x, y) val op ===> = Library.foldr op ==> fun sortify_typ sort (Type (tyco, args)) = Type (tyco, map (sortify_typ sort) args) | sortify_typ sort (TFree (name, _)) = TFree (name, sort) | sortify_typ _ (TVar _) = error "TVar encountered" fun sortify sort (Const (name, typ)) = Const (name, sortify_typ sort typ) | sortify sort (Free (name, typ)) = Free (name, sortify_typ sort typ) | sortify sort (t $ u) = sortify sort t $ sortify sort u | sortify sort (Abs (name, typ, term)) = Abs (name, sortify_typ sort typ, sortify sort term) | sortify _ (Bound n) = Bound n | sortify _ (Var _) = error "Var encountered" val typify_typ = sortify_typ @{sort type} val typify = sortify @{sort type} fun all_frees (Free (name, typ)) = [(name, typ)] | all_frees (t $ u) = union (op =) (all_frees t) (all_frees u) | all_frees (Abs (_, _, t)) = all_frees t | all_frees _ = [] val all_frees' = map fst o all_frees fun all_tfrees (TFree (name, sort)) = [(name, sort)] | all_tfrees (Type (_, ts)) = fold (union (op =)) (map all_tfrees ts) [] | all_tfrees _ = [] (* printing *) fun pretty_const ctxt const = Syntax.pretty_term ctxt (Const (const, Sign.the_const_type (Proof_Context.theory_of ctxt) const)) (* conversion/tactic *) fun ANY tacs = fold (curry op APPEND) tacs no_tac fun ANY' tacs n = fold (curry op APPEND) (map (fn t => t n) tacs) no_tac fun TRY' tac n = TRY (tac n) fun descend_fun_conv cv = cv else_conv (fn ct => case Thm.term_of ct of _ $ _ => Conv.fun_conv (descend_fun_conv cv) ct | _ => Conv.no_conv ct) fun lhs_conv cv = cv |> Conv.arg1_conv |> Conv.arg_conv fun rhs_conv cv = cv |> Conv.arg_conv |> Conv.arg_conv fun rewr_lhs_head_conv thm = safe_mk_meta_eq thm |> Conv.rewr_conv |> descend_fun_conv |> lhs_conv fun rewr_rhs_head_conv thm = safe_mk_meta_eq thm |> Conv.rewr_conv |> descend_fun_conv |> rhs_conv fun conv_result cv ct = Thm.prop_of (cv ct) |> Logic.dest_equals |> snd fun changed_conv cv = fn ct => let val res = cv ct val (lhs, rhs) = Thm.prop_of res |> Logic.dest_equals in if lhs aconv rhs then raise CTERM ("no conversion", []) else res end fun multi_induct_tac rules insts arbitrary ctxt = let val insts' = map (map (SOME o pair NONE o rpair false)) insts val arbitrary' = map (map dest_Free) arbitrary in DETERM (Induct.induct_tac ctxt false insts' arbitrary' [] (SOME rules) [] 1) end fun maybe_induct_tac (SOME rules) insts arbitrary = multi_induct_tac rules insts arbitrary | maybe_induct_tac NONE _ _ = K all_tac fun (tac CONTINUE_WITH tacs) i st = st |> (tac i THEN (fn st' => let val n' = Thm.nprems_of st' val n = Thm.nprems_of st fun aux [] _ = all_tac | aux (tac :: tacs) i = tac i THEN aux tacs (i - 1) in if n' - n + 1 <> length tacs then raise THM ("CONTINUE_WITH: unexpected number of emerging subgoals", 0, [st']) else aux (rev tacs) (i + n' - n) st' end)) fun (tac CONTINUE_WITH_FW tacs) i st = st |> (tac i THEN (fn st' => let val n' = Thm.nprems_of st' val n = Thm.nprems_of st fun aux [] _ st = all_tac st | aux (tac :: tacs) i st = st |> (tac i THEN (fn st' => aux tacs (i + 1 + Thm.nprems_of st' - Thm.nprems_of st) st')) in if n' - n + 1 <> length tacs then raise THM ("unexpected number of emerging subgoals", 0, [st']) else aux tacs i st' end)) fun SOLVED tac = tac THEN ALLGOALS (K no_tac) fun print_tac' ctxt str = SELECT_GOAL (print_tac ctxt str) fun fo_cong_tac ctxt thm = SUBGOAL (fn (concl, i) => let val lhs_of = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst val concl_pat = lhs_of (Thm.concl_of thm) |> Thm.cterm_of ctxt val concl = lhs_of concl |> Thm.cterm_of ctxt val insts = Thm.first_order_match (concl_pat, concl) in resolve_tac ctxt [Drule.instantiate_normalize insts thm] i end handle Pattern.MATCH => no_tac) (* theorem manipulation *) fun contract ctxt thm = let val (((_, frees), [thm']), ctxt') = Variable.import true [thm] ctxt val prop = Thm.prop_of thm' val prems = Logic.strip_imp_prems prop val (lhs, rhs) = Logic.strip_imp_concl prop |> HOLogic.dest_Trueprop |> HOLogic.dest_eq fun used x = exists (exists_subterm (fn t => t = x)) prems val (f, xs) = strip_comb lhs val (g, ys) = strip_comb rhs fun loop [] ys = (0, (f, list_comb (g, rev ys))) | loop xs [] = (0, (list_comb (f, rev xs), g)) | loop (x :: xs) (y :: ys) = if x = y andalso is_Free x andalso not (used x) then loop xs ys |> apfst (fn x => x + 1) else (0, (list_comb (f, rev (x :: xs)), list_comb (g, rev (y :: ys)))) val (count, (lhs', rhs')) = loop (rev xs) (rev ys) val concl' = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs')) fun tac ctxt 0 = resolve_tac ctxt [thm] THEN_ALL_NEW (Method.assm_tac ctxt) | tac ctxt n = resolve_tac ctxt @{thms ext} THEN' tac ctxt (n - 1) val prop = prems ===> concl' in Goal.prove_future ctxt' [] [] prop (fn {context, ...} => HEADGOAL (tac context count)) |> singleton (Variable.export ctxt' ctxt) end fun on_thms_complete f thms = (Future.fork (fn () => (Thm.consolidate thms; f ())); thms) (* theory *) fun define_params_nosyn term = Specification.definition NONE [] [] ((Binding.empty, []), term) #>> snd #>> snd fun note_thm binding thm = Local_Theory.note ((binding, []), [thm]) #>> snd #>> the_single fun note_thms binding thms = Local_Theory.note ((binding, []), thms) #>> snd (* timing *) fun with_timeout time f x = - case Exn.interruptible_capture (Timeout.apply time f) x of + case Exn.result (Timeout.apply time f) x of Exn.Res y => y | Exn.Exn (Timeout.TIMEOUT _) => x | Exn.Exn e => Exn.reraise e (* debugging *) val debug = Attrib.setup_config_bool @{binding "dict_construction_debug"} (K false) fun if_debug ctxt f = if Config.get ctxt debug then f () else () fun ALLGOALS' ctxt = if Config.get ctxt debug then ALLGOALS else PARALLEL_ALLGOALS fun prove' ctxt = if Config.get ctxt debug then Goal.prove ctxt else Goal.prove_future ctxt fun prove_common' ctxt = Goal.prove_common ctxt (if Config.get ctxt debug then NONE else SOME ~1) end \ No newline at end of file diff --git a/thys/Dict_Construction/transfer_termination.ML b/thys/Dict_Construction/transfer_termination.ML --- a/thys/Dict_Construction/transfer_termination.ML +++ b/thys/Dict_Construction/transfer_termination.ML @@ -1,154 +1,154 @@ signature TRANSFER_TERMINATION = sig val termination_tac: Function.info -> Function.info -> Proof.context -> int -> tactic end structure Transfer_Termination : TRANSFER_TERMINATION = struct open Dict_Construction_Util fun termination_tac ({R = new_R, ...}: Function.info) (old_info: Function.info) ctxt = let fun fallback_tac warn _ = (if warn then warning "Falling back to another termination proof" else (); Seq.empty) fun map_comp_bnf typ = let (* we start from a fresh lthy to avoid local hyps interfering with BNF *) val lthy = Proof_Context.theory_of ctxt |> Named_Target.theory_init |> Config.put BNF_Comp.typedef_threshold ~1 (* we just pretend that they're all live here *) val live_As = all_tfrees typ fun flatten_tyargs Ass = live_As |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) (* Dont_Inline would create new definitions, always *) val ((bnf, _), ((_, {map_unfolds, ...}), _)) = BNF_Comp.bnf_of_typ false BNF_Def.Do_Inline I flatten_tyargs live_As [] typ ((BNF_Comp.empty_comp_cache, BNF_Comp.empty_unfolds), lthy) val subst = map (Logic.dest_equals o Thm.prop_of) map_unfolds val t = BNF_Def.map_of_bnf bnf in (live_As, Envir.expand_term_defs dest_Const (map (apfst dest_Const) subst) t) end val tac = case old_info of {R = old_R, totality = SOME totality, ...} => let fun get_eq R = Inductive.the_inductive ctxt R |> snd |> #eqs |> the_single |> Local_Defs.abs_def_rule ctxt val (old_R_eq, new_R_eq) = apply2 get_eq (old_R, new_R) fun get_typ R = fastype_of R |> strip_type |> fst |> hd |> Type.legacy_freeze_type val (old_R_typ, new_R_typ) = apply2 get_typ (old_R, new_R) (* simple strategy: old_R and new_R are identical *) val simple_tac = let val totality' = Local_Defs.unfold ctxt [old_R_eq] totality in Local_Defs.unfold_tac ctxt [new_R_eq] THEN HEADGOAL (SOLVED' (resolve_tac ctxt [totality'])) end (* smart strategy: new_R can be simulated by old_R *) (* FIXME this is trigger-happy *) - val smart_tac = Exn.interruptible_capture (fn st => + val smart_tac = Exn.result (fn st => let val old_R_stripped = Thm.prop_of old_R_eq |> Logic.dest_equals |> snd |> map_types (K dummyT) |> Syntax.check_term ctxt val futile = old_R_stripped |> exists_type (exists_subtype (fn TFree (_, sort) => sort <> @{sort type} | TVar (_, sort) => sort <> @{sort type} | _ => false)) fun costrip_prodT new_t old_t = if Type.could_match (old_t, new_t) then (0, new_t) else case costrip_prodT (snd (HOLogic.dest_prodT new_t)) old_t of (n, stripped_t) => (n + 1, stripped_t) fun construct_inner_proj new_t old_t = let val (diff, stripped_t) = costrip_prodT new_t old_t val (tfrees, f_head) = map_comp_bnf stripped_t val f_args = map (K (Abs ("x", dummyT, Const (@{const_name undefined}, dummyT)))) tfrees fun add_snd 0 = list_comb (map_types (K dummyT) f_head, f_args) | add_snd n = Const (@{const_name comp}, dummyT) $ add_snd (n - 1) $ Const (@{const_name snd}, dummyT) in add_snd diff end fun construct_outer_proj new_t old_t = case (new_t, old_t) of (Type (@{type_name sum}, new_ts), Type (@{type_name sum}, old_ts)) => let val ps = map2 construct_outer_proj new_ts old_ts in list_comb (Const (@{const_name map_sum}, dummyT), ps) end | _ => construct_inner_proj new_t old_t val outer_proj = construct_outer_proj new_R_typ old_R_typ val old_R_typ_imported = yield_singleton Variable.importT_terms old_R ctxt |> fst |> get_typ val c = outer_proj |> Type.constraint (new_R_typ --> old_R_typ_imported) |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val wf_simulate = Drule.infer_instantiate ctxt [(("g", 0), c)] @{thm wf_simulate_simple} val old_wf = (@{thm wfP_implies_wf_set_of} OF [@{thm accp_wfPI} OF [totality]]) val inner_tac = match_tac ctxt @{thms wf_implies_dom} THEN' match_tac ctxt [wf_simulate] CONTINUE_WITH_FW [resolve_tac ctxt [old_wf], match_tac ctxt @{thms set_ofI} THEN' dmatch_tac ctxt @{thms set_ofD} THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt [old_R_eq, new_R_eq]) THEN' TRY' (REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE exE}) THEN' hyp_subst_tac_thin true ctxt THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms conjI exI}))] val unfold_tac = Local_Defs.unfold_tac ctxt @{thms comp_apply id_apply prod.sel} THEN auto_tac ctxt val tac = SOLVED (HEADGOAL inner_tac THEN unfold_tac) in if futile then (warning "Termination relation has sort constraints; termination proof is unlikely to be automatic or may even be impossible"; Seq.empty) else (tracing "Trying to re-use termination proof"; tac st) end) #> Exn.get_res #> the_default Seq.empty in simple_tac ORELSE smart_tac ORELSE fallback_tac true end | _ => fallback_tac false in SELECT_GOAL tac end end \ No newline at end of file diff --git a/thys/Native_Word/Uint64.thy b/thys/Native_Word/Uint64.thy --- a/thys/Native_Word/Uint64.thy +++ b/thys/Native_Word/Uint64.thy @@ -1,889 +1,889 @@ (* Title: Uint64.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 64 bits\ theory Uint64 imports Word_Type_Copies Code_Target_Integer_Bit begin text \ PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode. Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations directly to the \verb$Word64$ structure provided by the Standard ML implementations. The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit version which does not suffer from a division bug found in PolyML 5.6. \ section \Type definition and primitive operations\ typedef uint64 = \UNIV :: 64 word set\ .. global_interpretation uint64: word_type_copy Abs_uint64 Rep_uint64 using type_definition_uint64 by (rule word_type_copy.intro) setup_lifting type_definition_uint64 declare uint64.of_word_of [code abstype] declare Quotient_uint64 [transfer_rule] instantiation uint64 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint64 :: uint64 is 0 . lift_definition one_uint64 :: uint64 is 1 . lift_definition plus_uint64 :: \uint64 \ uint64 \ uint64\ is \(+)\ . lift_definition uminus_uint64 :: \uint64 \ uint64\ is uminus . lift_definition minus_uint64 :: \uint64 \ uint64 \ uint64\ is \(-)\ . lift_definition times_uint64 :: \uint64 \ uint64 \ uint64\ is \(*)\ . lift_definition divide_uint64 :: \uint64 \ uint64 \ uint64\ is \(div)\ . lift_definition modulo_uint64 :: \uint64 \ uint64 \ uint64\ is \(mod)\ . lift_definition equal_uint64 :: \uint64 \ uint64 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint64 :: \uint64 \ uint64 \ bool\ is \(\)\ . lift_definition less_uint64 :: \uint64 \ uint64 \ bool\ is \(<)\ . global_interpretation uint64: word_type_copy_ring Abs_uint64 Rep_uint64 by standard (fact zero_uint64.rep_eq one_uint64.rep_eq plus_uint64.rep_eq uminus_uint64.rep_eq minus_uint64.rep_eq times_uint64.rep_eq divide_uint64.rep_eq modulo_uint64.rep_eq equal_uint64.rep_eq less_eq_uint64.rep_eq less_uint64.rep_eq)+ instance proof - show \OFCLASS(uint64, comm_ring_1_class)\ by (rule uint64.of_class_comm_ring_1) show \OFCLASS(uint64, semiring_modulo_class)\ by (fact uint64.of_class_semiring_modulo) show \OFCLASS(uint64, equal_class)\ by (fact uint64.of_class_equal) show \OFCLASS(uint64, linorder_class)\ by (fact uint64.of_class_linorder) qed end instantiation uint64 :: ring_bit_operations begin lift_definition bit_uint64 :: \uint64 \ nat \ bool\ is bit . lift_definition not_uint64 :: \uint64 \ uint64\ is \Bit_Operations.not\ . lift_definition and_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.and\ . lift_definition or_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.or\ . lift_definition xor_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.xor\ . lift_definition mask_uint64 :: \nat \ uint64\ is mask . lift_definition push_bit_uint64 :: \nat \ uint64 \ uint64\ is push_bit . lift_definition drop_bit_uint64 :: \nat \ uint64 \ uint64\ is drop_bit . lift_definition signed_drop_bit_uint64 :: \nat \ uint64 \ uint64\ is signed_drop_bit . lift_definition take_bit_uint64 :: \nat \ uint64 \ uint64\ is take_bit . lift_definition set_bit_uint64 :: \nat \ uint64 \ uint64\ is Bit_Operations.set_bit . lift_definition unset_bit_uint64 :: \nat \ uint64 \ uint64\ is unset_bit . lift_definition flip_bit_uint64 :: \nat \ uint64 \ uint64\ is flip_bit . global_interpretation uint64: word_type_copy_bits Abs_uint64 Rep_uint64 signed_drop_bit_uint64 by standard (fact bit_uint64.rep_eq not_uint64.rep_eq and_uint64.rep_eq or_uint64.rep_eq xor_uint64.rep_eq mask_uint64.rep_eq push_bit_uint64.rep_eq drop_bit_uint64.rep_eq signed_drop_bit_uint64.rep_eq take_bit_uint64.rep_eq set_bit_uint64.rep_eq unset_bit_uint64.rep_eq flip_bit_uint64.rep_eq)+ instance by (fact uint64.of_class_ring_bit_operations) end lift_definition uint64_of_nat :: \nat \ uint64\ is word_of_nat . lift_definition nat_of_uint64 :: \uint64 \ nat\ is unat . lift_definition uint64_of_int :: \int \ uint64\ is word_of_int . lift_definition int_of_uint64 :: \uint64 \ int\ is uint . context includes integer.lifting begin lift_definition Uint64 :: \integer \ uint64\ is word_of_int . lift_definition integer_of_uint64 :: \uint64 \ integer\ is uint . end global_interpretation uint64: word_type_copy_more Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 apply standard apply (simp_all add: uint64_of_nat.rep_eq nat_of_uint64.rep_eq uint64_of_int.rep_eq int_of_uint64.rep_eq Uint64.rep_eq integer_of_uint64.rep_eq integer_eq_iff) done instantiation uint64 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint64 :: \uint64 \ nat\ is size . lift_definition msb_uint64 :: \uint64 \ bool\ is msb . lift_definition lsb_uint64 :: \uint64 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint64 :: \uint64 \ nat \ bool \ uint64\ where set_bit_uint64_eq: \set_bit_uint64 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint64_transfer [transfer_rule]: \(cr_uint64 ===> (=) ===> (\) ===> cr_uint64) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint64_eq [abs_def]) transfer_prover end lift_definition set_bits_uint64 :: \(nat \ bool) \ uint64\ is set_bits . lift_definition set_bits_aux_uint64 :: \(nat \ bool) \ nat \ uint64 \ uint64\ is set_bits_aux . global_interpretation uint64: word_type_copy_misc Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 64 set_bits_aux_uint64 by (standard; transfer) simp_all instance using uint64.of_class_bit_comprehension uint64.of_class_set_bit uint64.of_class_lsb by simp_all standard end section \Code setup\ text \ For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$. If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume that there is also a \Word64\ structure available and accordingly replace the implementation for the target \verb$Eval$. \ code_printing code_module "Uint64" \ (SML) \(* Test that words can handle numbers between 0 and 63 *) val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6")); structure Uint64 : sig eqtype uint64; val zero : uint64; val one : uint64; val fromInt : IntInf.int -> uint64; val toInt : uint64 -> IntInf.int; val toLarge : uint64 -> LargeWord.word; val fromLarge : LargeWord.word -> uint64 val plus : uint64 -> uint64 -> uint64; val minus : uint64 -> uint64 -> uint64; val times : uint64 -> uint64 -> uint64; val divide : uint64 -> uint64 -> uint64; val modulus : uint64 -> uint64 -> uint64; val negate : uint64 -> uint64; val less_eq : uint64 -> uint64 -> bool; val less : uint64 -> uint64 -> bool; val notb : uint64 -> uint64; val andb : uint64 -> uint64 -> uint64; val orb : uint64 -> uint64 -> uint64; val xorb : uint64 -> uint64 -> uint64; val shiftl : uint64 -> IntInf.int -> uint64; val shiftr : uint64 -> IntInf.int -> uint64; val shiftr_signed : uint64 -> IntInf.int -> uint64; val set_bit : uint64 -> IntInf.int -> bool -> uint64; val test_bit : uint64 -> IntInf.int -> bool; end = struct type uint64 = IntInf.int; val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int; val zero = 0 : IntInf.int; val one = 1 : IntInf.int; fun fromInt x = IntInf.andb(x, mask); fun toInt x = x fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x); fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x); fun plus x y = IntInf.andb(IntInf.+(x, y), mask); fun minus x y = IntInf.andb(IntInf.-(x, y), mask); fun negate x = IntInf.andb(IntInf.~(x), mask); fun times x y = IntInf.andb(IntInf.*(x, y), mask); fun divide x y = IntInf.div(x, y); fun modulus x y = IntInf.mod(x, y); fun less_eq x y = IntInf.<=(x, y); fun less x y = IntInf.<(x, y); fun notb x = IntInf.andb(IntInf.notb(x), mask); fun orb x y = IntInf.orb(x, y); fun andb x y = IntInf.andb(x, y); fun xorb x y = IntInf.xorb(x, y); val maxWord = IntInf.pow (2, Word.wordSize); fun shiftl x n = if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask) else 0; fun shiftr x n = if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) else 0; val msb_mask = 0x8000000000000000 : IntInf.int; fun shiftr_signed x i = if IntInf.andb(x, msb_mask) = 0 then shiftr x i else if i >= 64 then 0xFFFFFFFFFFFFFFFF else let val x' = shiftr x i val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask) in IntInf.orb(x', m') end; fun test_bit x n = if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0 else false; fun set_bit x n b = if n < 64 then if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))) else x; end \ code_reserved SML Uint64 setup \ let val polyml64 = LargeWord.wordSize > 63; (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain from using Word64 in that case. Testing is done with dynamic code evaluation such that the compiler does not choke on the Word64 structure, which need not be present in a 32bit environment. *) val error_msg = "Buggy Word64 structure"; val test_code = "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^ "else raise (Fail \"" ^ error_msg ^ "\");"; - val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code)) + val f = Exn.result (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code)) val use_Word64 = polyml64 andalso (case f () of Exn.Res _ => true | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e | Exn.Exn e => Exn.reraise e) ; val newline = "\n"; val content = "structure Uint64 : sig" ^ newline ^ " eqtype uint64;" ^ newline ^ " val zero : uint64;" ^ newline ^ " val one : uint64;" ^ newline ^ " val fromInt : IntInf.int -> uint64;" ^ newline ^ " val toInt : uint64 -> IntInf.int;" ^ newline ^ " val toLarge : uint64 -> LargeWord.word;" ^ newline ^ " val fromLarge : LargeWord.word -> uint64" ^ newline ^ " val plus : uint64 -> uint64 -> uint64;" ^ newline ^ " val minus : uint64 -> uint64 -> uint64;" ^ newline ^ " val times : uint64 -> uint64 -> uint64;" ^ newline ^ " val divide : uint64 -> uint64 -> uint64;" ^ newline ^ " val modulus : uint64 -> uint64 -> uint64;" ^ newline ^ " val negate : uint64 -> uint64;" ^ newline ^ " val less_eq : uint64 -> uint64 -> bool;" ^ newline ^ " val less : uint64 -> uint64 -> bool;" ^ newline ^ " val notb : uint64 -> uint64;" ^ newline ^ " val andb : uint64 -> uint64 -> uint64;" ^ newline ^ " val orb : uint64 -> uint64 -> uint64;" ^ newline ^ " val xorb : uint64 -> uint64 -> uint64;" ^ newline ^ " val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^ " val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^ "end = struct" ^ newline ^ "" ^ newline ^ "type uint64 = Word64.word;" ^ newline ^ "" ^ newline ^ "val zero = (0wx0 : uint64);" ^ newline ^ "" ^ newline ^ "val one = (0wx1 : uint64);" ^ newline ^ "" ^ newline ^ "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^ "" ^ newline ^ "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);" ^ newline ^ "" ^ newline ^ "fun fromLarge x = Word64.fromLarge x;" ^ newline ^ "" ^ newline ^ "fun toLarge x = Word64.toLarge x;" ^ newline ^ "" ^ newline ^ "fun plus x y = Word64.+(x, y);" ^ newline ^ "" ^ newline ^ "fun minus x y = Word64.-(x, y);" ^ newline ^ "" ^ newline ^ "fun negate x = Word64.~(x);" ^ newline ^ "" ^ newline ^ "fun times x y = Word64.*(x, y);" ^ newline ^ "" ^ newline ^ "fun divide x y = Word64.div(x, y);" ^ newline ^ "" ^ newline ^ "fun modulus x y = Word64.mod(x, y);" ^ newline ^ "" ^ newline ^ "fun less_eq x y = Word64.<=(x, y);" ^ newline ^ "" ^ newline ^ "fun less x y = Word64.<(x, y);" ^ newline ^ "" ^ newline ^ "fun set_bit x n b =" ^ newline ^ " let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ " in if b then Word64.orb (x, mask)" ^ newline ^ " else Word64.andb (x, Word64.notb mask)" ^ newline ^ " end" ^ newline ^ "" ^ newline ^ "fun shiftl x n =" ^ newline ^ " Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr x n =" ^ newline ^ " Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr_signed x n =" ^ newline ^ " Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun test_bit x n =" ^ newline ^ " Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^ "" ^ newline ^ "val notb = Word64.notb" ^ newline ^ "" ^ newline ^ "fun andb x y = Word64.andb(x, y);" ^ newline ^ "" ^ newline ^ "fun orb x y = Word64.orb(x, y);" ^ newline ^ "" ^ newline ^ "fun xorb x y = Word64.xorb(x, y);" ^ newline ^ "" ^ newline ^ "end (*struct Uint64*)" val target_SML64 = "SML_word"; in (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I) #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))])) end \ code_printing code_module Uint64 \ (Haskell) \module Uint64(Int64, Word64) where import Data.Int(Int64) import Data.Word(Word64)\ code_reserved Haskell Uint64 text \ OCaml and Scala provide only signed 64bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint64" \ (OCaml) \module Uint64 : sig val less : int64 -> int64 -> bool val less_eq : int64 -> int64 -> bool val set_bit : int64 -> Z.t -> bool -> int64 val shiftl : int64 -> Z.t -> int64 val shiftr : int64 -> Z.t -> int64 val shiftr_signed : int64 -> Z.t -> int64 val test_bit : int64 -> Z.t -> bool end = struct (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y < 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;; let less_eq x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;; let set_bit x n b = let mask = Int64.shift_left Int64.one (Z.to_int n) in if b then Int64.logor x mask else Int64.logand x (Int64.lognot mask);; let shiftl x n = Int64.shift_left x (Z.to_int n);; let shiftr x n = Int64.shift_right_logical x (Z.to_int n);; let shiftr_signed x n = Int64.shift_right x (Z.to_int n);; let test_bit x n = Int64.compare (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n))) Int64.zero <> 0;; end;; (*struct Uint64*)\ code_reserved OCaml Uint64 code_printing code_module Uint64 \ (Scala) \object Uint64 { def less(x: Long, y: Long) : Boolean = if (x < 0) y < 0 && x < y else y < 0 || x < y def less_eq(x: Long, y: Long) : Boolean = if (x < 0) y < 0 && x <= y else y < 0 || x <= y def set_bit(x: Long, n: BigInt, b: Boolean) : Long = if (b) x | (1L << n.intValue) else x & (1L << n.intValue).unary_~ def shiftl(x: Long, n: BigInt) : Long = x << n.intValue def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue def test_bit(x: Long, n: BigInt) : Boolean = (x & (1L << n.intValue)) != 0 } /* object Uint64 */\ code_reserved Scala Uint64 text \ OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer. The following justifies the implementation. \ context includes bit_operations_syntax begin definition Uint64_signed :: "integer \ uint64" where "Uint64_signed i = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then undefined Uint64 i else Uint64 i)" lemma Uint64_code [code]: "Uint64 i = (let i' = i AND 0xFFFFFFFFFFFFFFFF in if bit i' 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')" including undefined_transfer integer.lifting unfolding Uint64_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong) done lemma Uint64_signed_code [code]: "Rep_uint64 (Uint64_signed i) = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))" unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def by(simp add: Abs_uint64_inverse) end text \ Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. The symbolic implementations for code\_simp use @{term Rep_uint64}. The new destructor @{term Rep_uint64'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint64} ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because these instances will be folded away.) To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}. \ definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64" lemma Rep_uint64'_transfer [transfer_rule]: "rel_fun cr_uint64 (=) (\x. x) Rep_uint64'" unfolding Rep_uint64'_def by(rule uint64.rep_transfer) lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint64' :: "64 word \ uint64" is "\x :: 64 word. x" . lemma Abs_uint64'_code [code]: "Abs_uint64' x = Uint64 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint64 \ _"]] lemma term_of_uint64_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []])) (term_of_class.term_of (Rep_uint64' x))" by(simp add: term_of_anything) code_printing type_constructor uint64 \ (SML) "Uint64.uint64" and (Haskell) "Uint64.Word64" and (OCaml) "int64" and (Scala) "Long" | constant Uint64 \ (SML) "Uint64.fromInt" and (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and (Scala) "_.longValue" | constant Uint64_signed \ (OCaml) "Z.to'_int64" | constant "0 :: uint64" \ (SML) "Uint64.zero" and (Haskell) "(0 :: Uint64.Word64)" and (OCaml) "Int64.zero" and (Scala) "0" | constant "1 :: uint64" \ (SML) "Uint64.one" and (Haskell) "(1 :: Uint64.Word64)" and (OCaml) "Int64.one" and (Scala) "1" | constant "plus :: uint64 \ _ " \ (SML) "Uint64.plus" and (Haskell) infixl 6 "+" and (OCaml) "Int64.add" and (Scala) infixl 7 "+" | constant "uminus :: uint64 \ _" \ (SML) "Uint64.negate" and (Haskell) "negate" and (OCaml) "Int64.neg" and (Scala) "!(- _)" | constant "minus :: uint64 \ _" \ (SML) "Uint64.minus" and (Haskell) infixl 6 "-" and (OCaml) "Int64.sub" and (Scala) infixl 7 "-" | constant "times :: uint64 \ _ \ _" \ (SML) "Uint64.times" and (Haskell) infixl 7 "*" and (OCaml) "Int64.mul" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint64 \ _ \ bool" \ (SML) "!((_ : Uint64.uint64) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Int64.compare _ _ = 0)" and (Scala) infixl 5 "==" | class_instance uint64 :: equal \ (Haskell) - | constant "less_eq :: uint64 \ _ \ bool" \ (SML) "Uint64.less'_eq" and (Haskell) infix 4 "<=" and (OCaml) "Uint64.less'_eq" and (Scala) "Uint64.less'_eq" | constant "less :: uint64 \ _ \ bool" \ (SML) "Uint64.less" and (Haskell) infix 4 "<" and (OCaml) "Uint64.less" and (Scala) "Uint64.less" | constant "Bit_Operations.not :: uint64 \ _" \ (SML) "Uint64.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Int64.lognot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint64 \ _" \ (SML) "Uint64.andb" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Int64.logand" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint64 \ _" \ (SML) "Uint64.orb" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Int64.logor" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint64 \ _" \ (SML) "Uint64.xorb" and (Haskell) "Data'_Bits.xor" and (OCaml) "Int64.logxor" and (Scala) infixl 2 "^" definition uint64_divmod :: "uint64 \ uint64 \ uint64 \ uint64" where "uint64_divmod x y = (if y = 0 then (undefined ((div) :: uint64 \ _) x (0 :: uint64), undefined ((mod) :: uint64 \ _) x (0 :: uint64)) else (x div y, x mod y))" definition uint64_div :: "uint64 \ uint64 \ uint64" where "uint64_div x y = fst (uint64_divmod x y)" definition uint64_mod :: "uint64 \ uint64 \ uint64" where "uint64_mod x y = snd (uint64_divmod x y)" lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)" including undefined_transfer unfolding uint64_divmod_def uint64_div_def by transfer (simp add: word_div_def) lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)" including undefined_transfer unfolding uint64_mod_def uint64_divmod_def by transfer (simp add: word_mod_def) definition uint64_sdiv :: "uint64 \ uint64 \ uint64" where [code del]: "uint64_sdiv x y = (if y = 0 then undefined ((div) :: uint64 \ _) x (0 :: uint64) else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))" definition div0_uint64 :: "uint64 \ uint64" where [code del]: "div0_uint64 x = undefined ((div) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: div0_uint64]] definition mod0_uint64 :: "uint64 \ uint64" where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: mod0_uint64]] lemma uint64_divmod_code [code]: "uint64_divmod x y = (if 0x8000000000000000 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint64 x, mod0_uint64 x) else let q = push_bit 1 (uint64_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def less_eq_uint64.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint64_sdiv_code [code]: "Rep_uint64 (uint64_sdiv x y) = (if y = 0 then Rep_uint64 (undefined ((div) :: uint64 \ _) x (0 :: uint64)) else Rep_uint64 x sdiv Rep_uint64 y)" unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint64_divmod_code} computes both with division only. \ code_printing constant uint64_div \ (SML) "Uint64.divide" and (Haskell) "Prelude.div" | constant uint64_mod \ (SML) "Uint64.modulus" and (Haskell) "Prelude.mod" | constant uint64_divmod \ (Haskell) "divmod" | constant uint64_sdiv \ (OCaml) "Int64.div" and (Scala) "_ '/ _" definition uint64_test_bit :: "uint64 \ integer \ bool" where [code del]: "uint64_test_bit x n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) x n else bit x (nat_of_integer n))" lemma bit_uint64_code [code]: "bit x n \ n < 64 \ uint64_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint64_test_bit_def by transfer (auto dest: bit_imp_le_length) lemma uint64_test_bit_code [code]: "uint64_test_bit w n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) w n else bit (Rep_uint64 w) (nat_of_integer n))" unfolding uint64_test_bit_def by(simp add: bit_uint64.rep_eq) code_printing constant uint64_test_bit \ (SML) "Uint64.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint64.test'_bit" and (Scala) "Uint64.test'_bit" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)" definition uint64_set_bit :: "uint64 \ integer \ bool \ uint64" where [code del]: "uint64_set_bit x n b = (if n < 0 \ 63 < n then undefined (set_bit :: uint64 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint64_code [code]: "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint64_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint64_set_bit_code [code]: "Rep_uint64 (uint64_set_bit w n b) = (if n < 0 \ 63 < n then Rep_uint64 (undefined (set_bit :: uint64 \ _) w n b) else set_bit (Rep_uint64 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint64_set_bit_def by transfer simp code_printing constant uint64_set_bit \ (SML) "Uint64.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint64.set'_bit" and (Scala) "Uint64.set'_bit" and (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)" definition uint64_shiftl :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftl x n = (if n < 0 \ 64 \ n then undefined (push_bit :: nat \ uint64 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint64_code [code]: "push_bit n x = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftl_def by transfer simp lemma uint64_shiftl_code [code]: "Rep_uint64 (uint64_shiftl w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (push_bit :: nat \ uint64 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftl_def by transfer simp code_printing constant uint64_shiftl \ (SML) "Uint64.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint64.shiftl" and (Scala) "Uint64.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)" definition uint64_shiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftr x n = (if n < 0 \ 64 \ n then undefined (drop_bit :: nat \ uint64 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint64_code [code]: "drop_bit n x = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftr_def by transfer simp lemma uint64_shiftr_code [code]: "Rep_uint64 (uint64_shiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (drop_bit :: nat \ uint64 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftr_def by transfer simp code_printing constant uint64_shiftr \ (SML) "Uint64.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint64.shiftr" and (Scala) "Uint64.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)" definition uint64_sshiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_sshiftr x n = (if n < 0 \ 64 \ n then undefined signed_drop_bit_uint64 n x else signed_drop_bit_uint64 (nat_of_integer n) x)" lemma sshiftr_uint64_code [code]: "signed_drop_bit_uint64 n x = (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if bit x 63 then - 1 else 0)" including undefined_transfer integer.lifting unfolding uint64_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond) lemma uint64_sshiftr_code [code]: "Rep_uint64 (uint64_sshiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined signed_drop_bit_uint64 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_sshiftr_def by transfer simp code_printing constant uint64_sshiftr \ (SML) "Uint64.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and (OCaml) "Uint64.shiftr'_signed" and (Scala) "Uint64.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint64_msb_test_bit: "msb x \ bit (x :: uint64) 63" by transfer (simp add: msb_word_iff_bit) lemma msb_uint64_code [code]: "msb x \ uint64_test_bit x 63" by (simp add: uint64_test_bit_def uint64_msb_test_bit) lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint64_code [code]: "int_of_uint64 x = int_of_integer (integer_of_uint64 x)" including integer.lifting by transfer simp lemma uint64_of_nat_code [code]: "uint64_of_nat = uint64_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint64_code [code]: "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)" unfolding integer_of_uint64_def including integer.lifting by transfer simp definition integer_of_uint64_signed :: "uint64 \ integer" where "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_uint64 n)" lemma integer_of_uint64_signed_code [code]: "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))" by (simp add: integer_of_uint64_signed_def integer_of_uint64_def) lemma integer_of_uint64_code [code]: "integer_of_uint64 n = (if bit n 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)" proof - have \integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 = Bit_Operations.set_bit 63 (integer_of_uint64_signed (take_bit 63 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint64 n = Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))\ if \bit n 63\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint64 n) m = bit (Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint64_signed_def bit_simps) qed end code_printing constant "integer_of_uint64" \ (SML) "Uint64.toInt" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint64_signed" \ (OCaml) "Z.of'_int64" and (Scala) "BigInt" section \Quickcheck setup\ definition uint64_of_natural :: "natural \ uint64" where "uint64_of_natural x \ Uint64 (integer_of_natural x)" instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint64 \ qc_random_cnv uint64_of_natural" definition "exhaustive_uint64 \ qc_exhaustive_cnv uint64_of_natural" definition "full_exhaustive_uint64 \ qc_full_exhaustive_cnv uint64_of_natural" instance .. end instantiation uint64 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0" "Typerep.Typerep (STR ''Uint64.uint64'') []" . definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint64 itself \ _"]] lemmas partial_term_of_uint64 [code] = partial_term_of_code instance .. end end