Loading theory "HOL-Library.Adhoc_Overloading" (required by "HOL-Imperative_HOL.Heap_Monad" via "HOL-Library.Monad_Syntax") Loading theory "HOL-Library.Char_ord" (required by "HOL-Library.Code_Char") Loading theory "HOL-Library.Code_Target_Int" Loading theory "HOL-Library.Code_Test" instantiation char :: linorder less_eq_char == less_eq :: char \ char \ bool less_char == less :: char \ char \ bool signature ADHOC_OVERLOADING = sig val generic_add_overloaded: string -> Context.generic -> Context.generic val generic_add_variant: string -> term -> Context.generic -> Context.generic val generic_remove_overloaded: string -> Context.generic -> Context.generic val generic_remove_variant: string -> term -> Context.generic -> Context.generic val is_overloaded: Proof.context -> string -> bool val show_variants: bool Config.T end structure Adhoc_Overloading: ADHOC_OVERLOADING ### theory "HOL-Library.Adhoc_Overloading" ### 0.088s elapsed time, 0.343s cpu time, 0.000s GC time Loading theory "HOL-Library.Monad_Syntax" (required by "HOL-Imperative_HOL.Heap_Monad") instantiation char :: distrib_lattice inf_char == inf :: char \ char \ char sup_char == sup :: char \ char \ char ### Code generator: dropping subsumed code equation ### 1 \ Int.Pos num.One ### Code generator: dropping subsumed code equation ### Int.Neg ?m + Int.Neg ?n \ Int.Neg (?m + ?n) ### Code generator: dropping subsumed code equation ### Int.Neg ?m + Int.Pos ?n \ Int.sub ?n ?m ### Code generator: dropping subsumed code equation ### Int.Pos ?m + Int.Neg ?n \ Int.sub ?m ?n ### Code generator: dropping subsumed code equation ### Int.Pos ?m + Int.Pos ?n \ Int.Pos (?m + ?n) ### Code generator: dropping subsumed code equation ### 0 + ?l \ ?l ### Code generator: dropping subsumed code equation ### ?k + 0 \ ?k ### Code generator: dropping subsumed code equation ### - Int.Neg ?m \ Int.Pos ?m ### Code generator: dropping subsumed code equation ### - Int.Pos ?m \ Int.Neg ?m ### Code generator: dropping subsumed code equation ### - 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m - Int.Neg ?n \ Int.sub ?n ?m ### Code generator: dropping subsumed code equation ### Int.Neg ?m - Int.Pos ?n \ Int.Neg (?m + ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m - Int.Neg ?n \ Int.Pos (?m + ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m - Int.Pos ?n \ Int.sub ?m ?n ### Code generator: dropping subsumed code equation ### 0 - ?l \ - ?l ### Code generator: dropping subsumed code equation ### ?k - 0 \ ?k ### Code generator: dropping subsumed code equation ### Int.dup (Int.Neg ?n) \ Int.Neg (num.Bit0 ?n) ### Code generator: dropping subsumed code equation ### Int.dup (Int.Pos ?n) \ Int.Pos (num.Bit0 ?n) ### Code generator: dropping subsumed code equation ### Int.dup 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m * Int.Neg ?n \ Int.Pos (?m * ?n) ### Code generator: dropping subsumed code equation ### Int.Neg ?m * Int.Pos ?n \ Int.Neg (?m * ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m * Int.Neg ?n \ Int.Neg (?m * ?n) instantiation String.literal :: linorder less_eq_literal == less_eq :: String.literal \ String.literal \ bool less_literal == less :: String.literal \ String.literal \ bool ### Code generator: dropping subsumed code equation ### Int.Pos ?m * Int.Pos ?n \ Int.Pos (?m * ?n) ### Code generator: dropping subsumed code equation ### 0 * ?l \ 0 ### Code generator: dropping subsumed code equation ### ?k * 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m div Int.Neg ?n \ fst (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m div Int.Neg ?n \ - Divides.adjust_div (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Neg ?m div Int.Pos ?n \ - Divides.adjust_div (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m div Int.Pos ?n \ fst (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### ?k div Int.Neg num.One \ - ?k ### Code generator: dropping subsumed code equation ### ?k div Int.Pos num.One \ ?k ### Code generator: dropping subsumed code equation ### 0 div ?k \ 0 ### Code generator: dropping subsumed code equation ### ?k div 0 \ 0 ### Code generator: dropping subsumed code equation ### Int.Neg ?m mod Int.Neg ?n \ - snd (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### Int.Pos ?m mod Int.Neg ?n \ ### - Divides.adjust_mod (Int.Pos ?n) (snd (divmod ?m ?n)) ### Code generator: dropping subsumed code equation ### Int.Neg ?m mod Int.Pos ?n \ ### Divides.adjust_mod (Int.Pos ?n) (snd (divmod ?m ?n)) ### Code generator: dropping subsumed code equation ### Int.Pos ?m mod Int.Pos ?n \ snd (divmod ?m ?n) ### Code generator: dropping subsumed code equation ### ?k mod Int.Neg num.One \ 0 ### Code generator: dropping subsumed code equation ### ?k mod Int.Pos num.One \ 0 ### Code generator: dropping subsumed code equation ### 0 mod ?k \ 0 ### Code generator: dropping subsumed code equation ### ?k mod 0 \ ?k ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) (num.Bit1 ?n) \ ### if ?m < ?n then (0, numeral (num.Bit1 ?m)) ### else divmod_step (num.Bit1 ?n) ### (divmod (num.Bit1 ?m) (num.Bit0 (num.Bit1 ?n))) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) (num.Bit1 ?n) \ ### if ?m \ ?n then (0, numeral (num.Bit0 ?m)) ### else divmod_step (num.Bit1 ?n) ### (divmod (num.Bit0 ?m) (num.Bit0 (num.Bit1 ?n))) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) (num.Bit0 ?n) \ ### case divmod ?m ?n of (q, r) \ (q, 2 * r + 1) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) (num.Bit0 ?n) \ ### case divmod ?m ?n of (q, r) \ (q, 2 * r) ### Code generator: dropping subsumed code equation ### divmod num.One (num.Bit1 ?n) \ (0, Numeral1) ### Code generator: dropping subsumed code equation ### divmod num.One (num.Bit0 ?n) \ (0, Numeral1) ### Code generator: dropping subsumed code equation ### divmod (num.Bit1 ?m) num.One \ (numeral (num.Bit1 ?m), 0) ### Code generator: dropping subsumed code equation ### divmod (num.Bit0 ?m) num.One \ (numeral (num.Bit0 ?m), 0) ### Code generator: dropping subsumed code equation ### divmod num.One num.One \ (Numeral1, 0) ### Code generator: dropping subsumed code equation ### equal_class.equal ?k ?k \ True ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Neg ?k) (Int.Neg ?l) \ equal_class.equal ?k ?l ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Neg ?k) (Int.Pos ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Neg ?k) 0 \ False ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Pos ?k) (Int.Neg ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Pos ?k) (Int.Pos ?l) \ equal_class.equal ?k ?l ### Code generator: dropping subsumed code equation ### equal_class.equal (Int.Pos ?k) 0 \ False ### Code generator: dropping subsumed code equation ### equal_class.equal 0 (Int.Neg ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal 0 (Int.Pos ?l) \ False ### Code generator: dropping subsumed code equation ### equal_class.equal 0 0 \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k \ Int.Neg ?l \ ?l \ ?k ### Code generator: dropping subsumed code equation ### Int.Neg ?k \ Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k \ 0 \ True ### Code generator: dropping subsumed code equation ### Int.Pos ?k \ Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### Int.Pos ?k \ Int.Pos ?l \ ?k \ ?l ### Code generator: dropping subsumed code equation ### Int.Pos ?k \ 0 \ False ### Code generator: dropping subsumed code equation ### 0 \ Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### 0 \ Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### 0 \ 0 \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k < Int.Neg ?l \ ?l < ?k ### Code generator: dropping subsumed code equation ### Int.Neg ?k < Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### Int.Neg ?k < 0 \ True ### Code generator: dropping subsumed code equation ### Int.Pos ?k < Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### Int.Pos ?k < Int.Pos ?l \ ?k < ?l ### Code generator: dropping subsumed code equation ### Int.Pos ?k < 0 \ False ### Code generator: dropping subsumed code equation ### 0 < Int.Neg ?l \ False ### Code generator: dropping subsumed code equation ### 0 < Int.Pos ?l \ True ### Code generator: dropping subsumed code equation ### 0 < 0 \ False ### theory "HOL-Library.Char_ord" ### 0.256s elapsed time, 0.979s cpu time, 0.000s GC time Loading theory "HOL-Library.Code_Char" ### Code generator: dropping subsumed code equation ### of_int (Int.Pos ?k) \ numeral ?k ### Code generator: dropping subsumed code equation ### of_int 0 \ 0::?'a ### Code generator: dropping subsumed code equation ### of_int (Int.Neg ?k) \ - numeral ?k ### Code generator: dropping subsumed code equation ### nat (Int.Pos ?k) \ nat_of_num ?k ### Code generator: dropping subsumed code equation ### nat 0 \ 0 ### Code generator: dropping subsumed code equation ### nat (Int.Neg ?k) \ 0 ### theory "HOL-Library.Code_Target_Int" ### 0.366s elapsed time, 1.399s cpu time, 0.000s GC time Loading theory "HOL-Library.Nat_Bijection" (required by "HOL-Imperative_HOL.Heap_Monad" via "HOL-Imperative_HOL.Heap" via "HOL-Library.Countable") ### theory "HOL-Library.Code_Char" ### 0.114s elapsed time, 0.435s cpu time, 0.000s GC time Loading theory "HOL-Library.Old_Datatype" (required by "HOL-Imperative_HOL.Heap_Monad" via "HOL-Imperative_HOL.Heap" via "HOL-Library.Countable") ### theory "HOL-Library.Monad_Syntax" ### 0.430s elapsed time, 1.640s cpu time, 0.000s GC time ### ML warning (line 182 of "~~/src/HOL/Tools/datatype_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 237 of "~~/src/HOL/Tools/datatype_realizer.ML"): ### Pattern is not exhaustive. signature DATATYPE_REALIZER = sig val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory end structure Datatype_Realizer: DATATYPE_REALIZER Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "size_list size <*mlex*> {}" ### theory "HOL-Library.Nat_Bijection" ### 0.760s elapsed time, 2.874s cpu time, 0.070s GC time signature CODE_TEST = sig val add_driver: string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory val end_markerN: string val eval_term: string -> Proof.context -> term -> term val evaluate: (theory -> Path.T -> string list -> string -> {compile_cmd: string option, files: (Path.T * string) list, mk_code_file: string -> Path.T, run_cmd: string}) -> (string * string) option -> string -> theory -> (string * string) list * string -> Path.T -> string val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string val failureN: string val ghc_options: string Config.T val overlord: bool Config.T val start_markerN: string val successN: string val target_Haskell: string val target_Scala: string val test_code_cmd: string list -> string list -> Proof.context -> unit val test_targets: Proof.context -> term list -> string list -> unit val test_terms: Proof.context -> term list -> string -> unit end structure Code_Test: CODE_TEST ### theory "HOL-Library.Code_Test" ### 1.313s elapsed time, 4.973s cpu time, 0.070s GC time ### ML warning (line 103 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. ### ML warning (line 129 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. ### ML warning (line 239 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. ### ML warning (line 252 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. ### ML warning (line 374 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. ### ML warning (line 663 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. ### ML warning (line 726 of "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"): ### Pattern is not exhaustive. signature OLD_DATATYPE = sig val add_datatype: config -> spec list -> theory -> string list * theory val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory val check_specs: spec list -> theory -> spec list * Proof.context type config = {quiet: bool, strict: bool} val default_config: config type descr = (int * (string * dtyp list * (string * dtyp list) list)) list val distinct_lemma: thm datatype dtyp = DtRec of int | DtTFree of string * sort | DtType of string * dtyp list type info = {case_cong: thm, case_cong_weak: thm, case_name: string, case_rewrites: thm list, descr: descr, distinct: thm list, exhaust: thm, index: int, induct: thm, inducts: thm list, inject: thm list, nchotomy: thm, rec_names: string list, rec_rewrites: thm list, split: thm, split_asm: thm} val read_specs: spec_cmd list -> theory -> spec list * Proof.context type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list val spec_cmd: spec_cmd parser type spec_cmd = (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list end structure Old_Datatype: OLD_DATATYPE ### ML warning (line 38 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (P) has not been referenced. ### ML warning (line 45 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (s) has not been referenced. ### ML warning (line 44 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 49 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (i) has not been referenced. ### ML warning (line 62 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 102 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 148 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (s) has not been referenced. ### ML warning (line 192 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (used) has not been referenced. ### ML warning (line 159 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 165 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 186 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (U) has not been referenced. ### ML warning (line 186 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (Ts) has not been referenced. ### ML warning (line 204 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (induct) has not been referenced. ### ML warning (line 227 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 228 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 243 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 325 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 340 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 348 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 367 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 384 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 392 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Matches are not exhaustive. ### ML warning (line 407 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. ### ML warning (line 431 of "~~/src/HOL/Tools/inductive_realizer.ML"): ### Pattern is not exhaustive. signature INDUCTIVE_REALIZER = sig val add_ind_realizers: string -> string list -> theory -> theory end structure InductiveRealizer: INDUCTIVE_REALIZER ### theory "HOL-Library.Old_Datatype" ### 1.580s elapsed time, 5.321s cpu time, 0.205s GC time Loading theory "HOL-Library.Countable" (required by "HOL-Imperative_HOL.Heap_Monad" via "HOL-Imperative_HOL.Heap") ### Additional type variable(s) in locale specification "countable": 'a class countable = type + assumes "ex_inj": "\to_nat. inj to_nat" Proofs for inductive predicate(s) "finite_item" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... val old_countable_datatype_tac = fn: Proof.context -> int -> tactic ### ML warning (line 93 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 139 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 143 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 145 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 156 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. signature BNF_LFP_COUNTABLE = sig val countable_datatype_tac: Proof.context -> tactic val derive_encode_injectives_thms: Proof.context -> string list -> thm list end structure BNF_LFP_Countable: BNF_LFP_COUNTABLE val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq val countable_tac = fn: Proof.context -> int -> tactic ### theory "HOL-Library.Countable" ### 1.227s elapsed time, 1.542s cpu time, 0.051s GC time Loading theory "HOL-Imperative_HOL.Heap" (required by "HOL-Imperative_HOL.Heap_Monad") consts addr_of_array :: "'a array \ nat" consts addr_of_ref :: "'a ref \ nat" ### theory "HOL-Imperative_HOL.Heap" ### 1.204s elapsed time, 1.696s cpu time, 0.093s GC time Loading theory "HOL-Imperative_HOL.Heap_Monad" consts execute :: "'a Heap \ heap \ ('a \ heap) option" consts fold_map :: "('a \ 'b Heap) \ 'a list \ 'b list Heap" ### theory "HOL-Imperative_HOL.Heap_Monad" ### 1.737s elapsed time, 2.503s cpu time, 0.112s GC time Loading theory "Native_Word.More_Bits_Int" ### Ignoring duplicate rewrite rule: ### ?y1 AND ?x1 AND ?z1 \ ?x1 AND ?y1 AND ?z1 consts bin_mask :: "nat \ int" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Proofs for inductive predicate(s) "wf_set_bits_int" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Metis: Unused theorems: "More_Bits_Int.int_shiftl_numeral_2" ### Ignoring duplicate rewrite rule: ### ?x1 BIT ?b1 >> Suc ?n1 \ ?x1 >> ?n1 ### Metis: Unused theorems: "Nat.neq0_conv", "Num.numeral_class.numeral.numeral_One", "Num.semiring_char_0_class.zero_neq_numeral" ### theory "Native_Word.More_Bits_Int" ### 1.570s elapsed time, 3.443s cpu time, 0.141s GC time Loading theory "Native_Word.Bits_Integer" Loading theory "Native_Word.Word_Misc" instantiation integer :: bitss msb_integer == msb :: integer \ bool test_bit_integer == test_bit :: integer \ nat \ bool lsb_integer == lsb :: integer \ bool set_bit_integer == set_bit :: integer \ nat \ bool \ integer set_bits_integer == set_bits :: (nat \ bool) \ integer shiftl_integer == shiftl :: integer \ nat \ integer shiftr_integer == shiftr :: integer \ nat \ integer bitNOT_integer == bitNOT :: integer \ integer bitAND_integer == bitAND :: integer \ integer \ integer bitOR_integer == bitOR :: integer \ integer \ integer bitXOR_integer == bitXOR :: integer \ integer \ integer ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g Found termination order: "(\p. size (snd p)) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### 0 OR ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y OR 0 \ ?y ### Ignoring duplicate rewrite rule: ### 0 XOR ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y XOR 0 \ ?y Found termination order: "(nat \ abs) <*mlex*> {}" ### Metis: Unused theorems: "Word.word_sint.Rep_inverse'", "Word.wi_hom_neg" locale quickcheck_narrowing_samples fixes a_of_integer :: "integer \ 'a \ 'a" and zero :: "'a" and tr :: "typerep" ### theory "Native_Word.Word_Misc" ### 1.283s elapsed time, 4.736s cpu time, 0.129s GC time Loading theory "Native_Word.Native_Word_Imperative_HOL" ### theory "Native_Word.Native_Word_Imperative_HOL" ### 0.893s elapsed time, 3.183s cpu time, 0.039s GC time ### Ignoring duplicate rewrite rule: ### ?y < ?n1 \ ?y mod ?n1 \ ?y ### Legacy feature! Old 'def' command -- use 'define' instead ### Metis: Unused theorems: "Word.word_less_def" ### Metis: Unused theorems: "Nat.semiring_1_class.of_nat_mult" ### Ignoring duplicate rewrite rule: ### 0 OR ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y OR 0 \ ?y datatype 'a ref = ref of 'a structure Bits_Integer: sig val set_bit: int -> int -> bool -> int val shiftl: int -> int -> int val shiftr: int -> int -> int val test_bit: int -> int -> bool end ROOT.ML:38: warning: Pattern 3 is redundant. Found near fun equal_boola p true = p | equal_boola p ... = not p | equal_boola ... = p | equal_boola ... = ... ROOT.ML:39: warning: Pattern 4 is redundant. Found near fun equal_boola p true = p | equal_boola p ... = not p | equal_boola ... = p | equal_boola ... = ... ROOT.ML:85: warning: Value identifier (times) has not been referenced. ROOT.ML:88: warning: Value identifier (one_power) has not been referenced. ROOT.ML:89: warning: Value identifier (times_power) has not been referenced. ROOT.ML:98: warning: Value identifier (semigroup_add_ab_semigroup_add) has not been referenced. ROOT.ML:102: warning: Value identifier (times_semigroup_mult) has not been referenced. ROOT.ML:108: warning: Value identifier (ab_semigroup_add_semiring) has not been referenced. ROOT.ML:110: warning: Value identifier (semigroup_mult_semiring) has not been referenced. ROOT.ML:126: warning: Value identifier (times_mult_zero) has not been referenced. ROOT.ML:135: warning: Value identifier (semigroup_add_monoid_add) has not been referenced. ROOT.ML:137: warning: Value identifier (zero_monoid_add) has not been referenced. ROOT.ML:142: warning: Value identifier (ab_semigroup_add_comm_monoid_add) has not been referenced. ROOT.ML:144: warning: Value identifier (monoid_add_comm_monoid_add) has not been referenced. ROOT.ML:150: warning: Value identifier (comm_monoid_add_semiring_0) has not been referenced. ROOT.ML:154: warning: Value identifier (semiring_semiring_0) has not been referenced. ROOT.ML:175: warning: Value identifier (semigroup_mult_monoid_mult) has not been referenced. ROOT.ML:177: warning: Value identifier (power_monoid_mult) has not been referenced. ROOT.ML:183: warning: Value identifier (monoid_mult_semiring_numeral) has not been referenced. ROOT.ML:187: warning: Value identifier (semiring_semiring_numeral) has not been referenced. ROOT.ML:191: warning: Value identifier (one_zero_neq_one) has not been referenced. ROOT.ML:192: warning: Value identifier (zero_zero_neq_one) has not been referenced. ROOT.ML:202: warning: Value identifier (zero_neq_one_semiring_1) has not been referenced. ROOT.ML:247: warning: Value identifier (inc) has not been referenced. ROOT.ML:247: warning: Value identifier (A_) has not been referenced. ROOT.ML:280: warning: Value identifier (A_) has not been referenced. ROOT.ML:277: warning: Value identifier (x22) has not been referenced. ROOT.ML:277: warning: Value identifier (x21) has not been referenced. ROOT.ML:277: warning: Value identifier (A_) has not been referenced. ROOT.ML:276: warning: Value identifier (x22) has not been referenced. ROOT.ML:276: warning: Value identifier (x21) has not been referenced. ROOT.ML:276: warning: Value identifier (A_) has not been referenced. structure Generated_Code: sig val bit_integer_test: bool type nat type num end ### ISABELLE_OCAML not set; skipped checking code for OCaml ### theory "Native_Word.Bits_Integer" ### 13.503s elapsed time, 15.739s cpu time, 0.311s GC time Loading theory "Native_Word.Code_Target_Bits_Int" ### theory "Native_Word.Code_Target_Bits_Int" ### 0.482s elapsed time, 1.809s cpu time, 0.037s GC time Loading theory "Native_Word.Uint" Testing conjecture with Quickcheck-random... Quickcheck found a counterexample: x = 1 y = 0 Loading theory "Native_Word.Uint16" Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: x = 0 y = - 1 Evaluated terms: x AND y = 0 x OR y = - 1 Loading theory "Native_Word.Uint32" Loading theory "Native_Word.Uint64" (required by "Native_Word.Native_Cast") instantiation dflt_size :: typerep typerep_dflt_size == typerep_class.typerep :: dflt_size itself \ typerep specification dflt_size_aux_g0: 0 < dflt_size_aux instantiation dflt_size :: len len_of_dflt_size == len_of :: dflt_size itself \ nat ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Word.word" found. ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. instantiation uint :: {comm_monoid_mult,neg_numeral,comm_ring,modulo} modulo_uint == modulo :: uint \ uint \ uint divide_uint == divide :: uint \ uint \ uint minus_uint == minus :: uint \ uint \ uint uminus_uint == uminus :: uint \ uint zero_uint == zero_class.zero :: uint plus_uint == plus :: uint \ uint \ uint one_uint == one_class.one :: uint times_uint == times :: uint \ uint \ uint ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. instantiation uint16 :: {comm_monoid_mult,neg_numeral,comm_ring,modulo} modulo_uint16 == modulo :: uint16 \ uint16 \ uint16 divide_uint16 == divide :: uint16 \ uint16 \ uint16 minus_uint16 == minus :: uint16 \ uint16 \ uint16 uminus_uint16 == uminus :: uint16 \ uint16 zero_uint16 == zero_class.zero :: uint16 plus_uint16 == plus :: uint16 \ uint16 \ uint16 one_uint16 == one_class.one :: uint16 times_uint16 == times :: uint16 \ uint16 \ uint16 instantiation uint32 :: {comm_monoid_mult,neg_numeral,comm_ring,modulo} modulo_uint32 == modulo :: uint32 \ uint32 \ uint32 divide_uint32 == divide :: uint32 \ uint32 \ uint32 minus_uint32 == minus :: uint32 \ uint32 \ uint32 uminus_uint32 == uminus :: uint32 \ uint32 zero_uint32 == zero_class.zero :: uint32 plus_uint32 == plus :: uint32 \ uint32 \ uint32 one_uint32 == one_class.one :: uint32 times_uint32 == times :: uint32 \ uint32 \ uint32 ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. instantiation uint64 :: {comm_monoid_mult,neg_numeral,comm_ring,modulo} modulo_uint64 == modulo :: uint64 \ uint64 \ uint64 divide_uint64 == divide :: uint64 \ uint64 \ uint64 minus_uint64 == minus :: uint64 \ uint64 \ uint64 uminus_uint64 == uminus :: uint64 \ uint64 zero_uint64 == zero_class.zero :: uint64 plus_uint64 == plus :: uint64 \ uint64 \ uint64 one_uint64 == one_class.one :: uint64 times_uint64 == times :: uint64 \ uint64 \ uint64 instantiation uint :: linorder less_eq_uint == less_eq :: uint \ uint \ bool less_uint == less :: uint \ uint \ bool instantiation uint :: bitss msb_uint == msb :: uint \ bool test_bit_uint == test_bit :: uint \ nat \ bool lsb_uint == lsb :: uint \ bool set_bit_uint == set_bit :: uint \ nat \ bool \ uint set_bits_uint == set_bits :: (nat \ bool) \ uint shiftl_uint == shiftl :: uint \ nat \ uint shiftr_uint == shiftr :: uint \ nat \ uint bitNOT_uint == bitNOT :: uint \ uint bitAND_uint == bitAND :: uint \ uint \ uint bitOR_uint == bitOR :: uint \ uint \ uint bitXOR_uint == bitXOR :: uint \ uint \ uint instantiation uint16 :: linorder less_eq_uint16 == less_eq :: uint16 \ uint16 \ bool less_uint16 == less :: uint16 \ uint16 \ bool instantiation uint32 :: linorder less_eq_uint32 == less_eq :: uint32 \ uint32 \ bool less_uint32 == less :: uint32 \ uint32 \ bool instantiation uint16 :: bitss msb_uint16 == msb :: uint16 \ bool test_bit_uint16 == test_bit :: uint16 \ nat \ bool lsb_uint16 == lsb :: uint16 \ bool set_bit_uint16 == set_bit :: uint16 \ nat \ bool \ uint16 set_bits_uint16 == set_bits :: (nat \ bool) \ uint16 shiftl_uint16 == shiftl :: uint16 \ nat \ uint16 shiftr_uint16 == shiftr :: uint16 \ nat \ uint16 bitNOT_uint16 == bitNOT :: uint16 \ uint16 bitAND_uint16 == bitAND :: uint16 \ uint16 \ uint16 bitOR_uint16 == bitOR :: uint16 \ uint16 \ uint16 bitXOR_uint16 == bitXOR :: uint16 \ uint16 \ uint16 instantiation uint32 :: bitss msb_uint32 == msb :: uint32 \ bool test_bit_uint32 == test_bit :: uint32 \ nat \ bool lsb_uint32 == lsb :: uint32 \ bool set_bit_uint32 == set_bit :: uint32 \ nat \ bool \ uint32 set_bits_uint32 == set_bits :: (nat \ bool) \ uint32 shiftl_uint32 == shiftl :: uint32 \ nat \ uint32 shiftr_uint32 == shiftr :: uint32 \ nat \ uint32 bitNOT_uint32 == bitNOT :: uint32 \ uint32 bitAND_uint32 == bitAND :: uint32 \ uint32 \ uint32 bitOR_uint32 == bitOR :: uint32 \ uint32 \ uint32 bitXOR_uint32 == bitXOR :: uint32 \ uint32 \ uint32 instantiation uint :: equal equal_uint == equal_class.equal :: uint \ uint \ bool instantiation uint :: size size_uint == size :: uint \ nat instantiation uint64 :: linorder less_eq_uint64 == less_eq :: uint64 \ uint64 \ bool less_uint64 == less :: uint64 \ uint64 \ bool instantiation uint64 :: bitss msb_uint64 == msb :: uint64 \ bool test_bit_uint64 == test_bit :: uint64 \ nat \ bool lsb_uint64 == lsb :: uint64 \ bool set_bit_uint64 == set_bit :: uint64 \ nat \ bool \ uint64 set_bits_uint64 == set_bits :: (nat \ bool) \ uint64 shiftl_uint64 == shiftl :: uint64 \ nat \ uint64 shiftr_uint64 == shiftr :: uint64 \ nat \ uint64 bitNOT_uint64 == bitNOT :: uint64 \ uint64 bitAND_uint64 == bitAND :: uint64 \ uint64 \ uint64 bitOR_uint64 == bitOR :: uint64 \ uint64 \ uint64 bitXOR_uint64 == bitXOR :: uint64 \ uint64 \ uint64 instantiation uint16 :: equal equal_uint16 == equal_class.equal :: uint16 \ uint16 \ bool instantiation uint16 :: size size_uint16 == size :: uint16 \ nat instantiation uint32 :: equal equal_uint32 == equal_class.equal :: uint32 \ uint32 \ bool instantiation uint32 :: size size_uint32 == size :: uint32 \ nat ### Code generator: dropping subsumed code equation ### op !! ?x \ op !! (Rep_uint ?x) ### Code generator: dropping subsumed code equation ### lsb ?x \ lsb (Rep_uint ?x) instantiation uint64 :: equal equal_uint64 == equal_class.equal :: uint64 \ uint64 \ bool ### Ambiguous input (line 725 of "~/repos/afp-2017/thys/Native_Word/Uint.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint.sshiftr_uint" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 729 of "~/repos/afp-2017/thys/Native_Word/Uint.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint.sshiftr_uint" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_position" dflt_size)) ### ("_applC" ("_position" uint_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_position" wivs_index)) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_position" dflt_size)) ### ("_applC" ("_position" uint_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_position" wivs_index)) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 736 of "~/repos/afp-2017/thys/Native_Word/Uint.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint) ### ("_applC" ("_position" uint_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_position" dflt_size_integer) ("_position" n))) ### ("_applC" ("_position" Rep_uint) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Word.sshiftr" ### ("_applC" ("_position" Rep_uint) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint) ### ("_applC" ("_position" uint_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_position" dflt_size_integer) ("_position" n))) ### ("_applC" ("_position" Rep_uint) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Uint.sshiftr_uint" ### ("_applC" ("_position" Rep_uint) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Code generator: dropping subsumed code equation ### msb ?x \ msb (Rep_uint ?x) instantiation uint64 :: size size_uint64 == size :: uint64 \ nat instantiation uint :: {exhaustive,full_exhaustive,random} random_uint == random_class.random :: natural \ natural \ natural \ (uint \ (unit \ term)) \ natural \ natural full_exhaustive_uint == full_exhaustive_class.full_exhaustive :: (uint \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option exhaustive_uint == exhaustive_class.exhaustive :: (uint \ (bool \ term list) option) \ natural \ (bool \ term list) option instantiation uint :: narrowing narrowing_uint == narrowing :: integer \ uint ??.Quickcheck_Narrowing.narrowing_cons ### Code generator: dropping subsumed code equation ### op !! ?x \ op !! (Rep_uint16 ?x) ### Code generator: dropping subsumed code equation ### lsb ?x \ lsb (Rep_uint16 ?x) ### Ambiguous input (line 449 of "~/repos/afp-2017/thys/Native_Word/Uint16.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint16.sshiftr_uint16" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 453 of "~/repos/afp-2017/thys/Native_Word/Uint16.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint16.sshiftr_uint16" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_Numeral" ("_constify" ("_position" 16)))) ### ("_applC" ("_position" uint16_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_Numeral" ("_constify" ("_position" 15)))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_Numeral" ("_constify" ("_position" 16)))) ### ("_applC" ("_position" uint16_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_Numeral" ("_constify" ("_position" 15)))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 459 of "~/repos/afp-2017/thys/Native_Word/Uint16.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint16) ### ("_applC" ("_position" uint16_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_Numeral" ("_constify" ("_position" 16))) ("_position" n))) ### ("_applC" ("_position" Rep_uint16) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint16) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Word.sshiftr" ### ("_applC" ("_position" Rep_uint16) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint16) ### ("_applC" ("_position" uint16_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_Numeral" ("_constify" ("_position" 16))) ("_position" n))) ### ("_applC" ("_position" Rep_uint16) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint16) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Uint16.sshiftr_uint16" ### ("_applC" ("_position" Rep_uint16) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Code generator: dropping subsumed code equation ### msb ?x \ msb (Rep_uint16 ?x) ### theory "Native_Word.Uint" ### 2.209s elapsed time, 8.337s cpu time, 0.191s GC time instantiation uint16 :: {exhaustive,full_exhaustive,random} random_uint16 == random_class.random :: natural \ natural \ natural \ (uint16 \ (unit \ term)) \ natural \ natural full_exhaustive_uint16 == full_exhaustive_class.full_exhaustive :: (uint16 \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option exhaustive_uint16 == exhaustive_class.exhaustive :: (uint16 \ (bool \ term list) option) \ natural \ (bool \ term list) option Loading theory "Native_Word.Uint8" ### Code generator: dropping subsumed code equation ### op !! ?x \ op !! (Rep_uint32 ?x) instantiation uint16 :: narrowing narrowing_uint16 == narrowing :: integer \ uint16 ??.Quickcheck_Narrowing.narrowing_cons ### Code generator: dropping subsumed code equation ### lsb ?x \ lsb (Rep_uint32 ?x) ### Ambiguous input (line 563 of "~/repos/afp-2017/thys/Native_Word/Uint32.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint32.sshiftr_uint32" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 567 of "~/repos/afp-2017/thys/Native_Word/Uint32.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint32.sshiftr_uint32" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_Numeral" ("_constify" ("_position" 32)))) ### ("_applC" ("_position" uint32_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_Numeral" ("_constify" ("_position" 31)))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_Numeral" ("_constify" ("_position" 32)))) ### ("_applC" ("_position" uint32_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_Numeral" ("_constify" ("_position" 31)))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 573 of "~/repos/afp-2017/thys/Native_Word/Uint32.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint32) ### ("_applC" ("_position" uint32_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_Numeral" ("_constify" ("_position" 32))) ("_position" n))) ### ("_applC" ("_position" Rep_uint32) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint32) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Word.sshiftr" ### ("_applC" ("_position" Rep_uint32) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint32) ### ("_applC" ("_position" uint32_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_Numeral" ("_constify" ("_position" 32))) ("_position" n))) ### ("_applC" ("_position" Rep_uint32) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint32) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Uint32.sshiftr_uint32" ### ("_applC" ("_position" Rep_uint32) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Code generator: dropping subsumed code equation ### msb ?x \ msb (Rep_uint32 ?x) instantiation uint32 :: {exhaustive,full_exhaustive,random} random_uint32 == random_class.random :: natural \ natural \ natural \ (uint32 \ (unit \ term)) \ natural \ natural full_exhaustive_uint32 == full_exhaustive_class.full_exhaustive :: (uint32 \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option exhaustive_uint32 == exhaustive_class.exhaustive :: (uint32 \ (bool \ term list) option) \ natural \ (bool \ term list) option instantiation uint32 :: narrowing narrowing_uint32 == narrowing :: integer \ uint32 ??.Quickcheck_Narrowing.narrowing_cons ### Code generator: dropping subsumed code equation ### op !! ?x \ op !! (Rep_uint64 ?x) ### theory "Native_Word.Uint16" ### 2.538s elapsed time, 9.461s cpu time, 0.286s GC time Testing conjecture with Quickcheck-narrowing... ### Code generator: dropping subsumed code equation ### lsb ?x \ lsb (Rep_uint64 ?x) ### Ambiguous input (line 761 of "~/repos/afp-2017/thys/Native_Word/Uint64.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint64.sshiftr_uint64" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less_eq" ### ("_applC" ("_position" size) ("_position" x)) ("_position" n))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("\<^const>Groups.minus_class.minus" ### ("_applC" ("_position" size) ("_position" x)) ### ("\<^const>Groups.one_class.one"))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 765 of "~/repos/afp-2017/thys/Native_Word/Uint64.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Uint64.sshiftr_uint64" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_Numeral" ("_constify" ("_position" 64)))) ### ("_applC" ("_position" uint64_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_Numeral" ("_constify" ("_position" 63)))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Word.sshiftr" ("_position" x) ("_position" n)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("_Numeral" ("_constify" ("_position" 64)))) ### ("_applC" ("_position" uint64_sshiftr) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" integer_of_nat) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>Bits.bits_class.test_bit" ("_position" x) ### ("_Numeral" ("_constify" ("_position" 63)))) ### ("\<^const>Groups.uminus_class.uminus" ### ("\<^const>Groups.one_class.one")) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 771 of "~/repos/afp-2017/thys/Native_Word/Uint64.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint64) ### ("_applC" ("_position" uint64_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_Numeral" ("_constify" ("_position" 64))) ("_position" n))) ### ("_applC" ("_position" Rep_uint64) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint64) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Word.sshiftr" ### ("_applC" ("_position" Rep_uint64) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Rep_uint64) ### ("_applC" ("_position" uint64_sshiftr) ### ("_cargs" ("_position" w) ("_position" n)))) ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>Orderings.ord_class.less" ("_position" n) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Orderings.ord_class.less_eq" ### ("_Numeral" ("_constify" ("_position" 64))) ("_position" n))) ### ("_applC" ("_position" Rep_uint64) ### ("_applC" ("_position" undefined) ### ("_cargs" ("_position" sshiftr_uint64) ### ("_cargs" ("_position" w) ("_position" n))))) ### ("\<^const>Uint64.sshiftr_uint64" ### ("_applC" ("_position" Rep_uint64) ("_position" w)) ### ("_applC" ("_position" nat_of_integer) ("_position" n)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Code generator: dropping subsumed code equation ### msb ?x \ msb (Rep_uint64 ?x) ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. ### theory "Native_Word.Uint32" ### 2.721s elapsed time, 10.189s cpu time, 0.286s GC time instantiation uint64 :: {exhaustive,full_exhaustive,random} random_uint64 == random_class.random :: natural \ natural \ natural \ (uint64 \ (unit \ term)) \ natural \ natural full_exhaustive_uint64 == full_exhaustive_class.full_exhaustive :: (uint64 \ (unit \ term) \ (bool \ term list) option) \