Loading theory "HOL-Eisbach.Eisbach" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib" via "Automatic_Refinement.Misc") Loading theory "Automatic_Refinement.Foldi" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature PARSE_TOOLS = sig val is_real_val: ('a, 'b) parse_val -> bool val name_term: (term, string) parse_val parser val parse_term_val: 'a parser -> (term, 'a) parse_val parser val parse_thm_val: 'a parser -> (thm, 'a) parse_val parser datatype ('a, 'b) parse_val = Parse_Val of 'b * ('a -> unit) | Real_Val of 'a val parse_val_cases: ('a -> 'b) -> ('b, 'a) parse_val -> 'b * ('b -> unit) val the_parse_fun: ('a, 'b) parse_val -> 'a -> unit val the_parse_val: ('a, 'b) parse_val -> 'b val the_real_val: ('a, 'b) parse_val -> 'a end structure Parse_Tools: PARSE_TOOLS consts foldli :: "'b list \ ('a \ bool) \ ('b \ 'a \ 'a) \ 'a \ 'a" signature METHOD_CLOSURE = sig val apply_method: Proof.context -> string -> term list -> thm list list -> (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic val method: binding -> (binding * typ option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> string * local_theory val method_cmd: binding -> (binding * string option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> string * local_theory end structure Method_Closure: METHOD_CLOSURE ### theory "Automatic_Refinement.Foldi" ### 0.221s elapsed time, 0.444s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Prio_List" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature PRIO_LIST = sig type T val add_after: T -> item -> item -> T val add_before: T -> item -> item -> T val add_first: T -> item -> T val add_last: T -> item -> T val contains: T -> item -> bool val delete: item -> T -> T val dest: T -> item list val empty: T type item val merge: T * T -> T val merge': T * T -> item list * T val prio_of: (item -> bool) -> (item * item -> bool) -> T -> int end functor Prio_List (sig val eq: item * item -> bool type item end): PRIO_LIST ### theory "Automatic_Refinement.Prio_List" ### 0.047s elapsed time, 0.092s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Refine_Util_Bootstrap1" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib" via "Automatic_Refinement.Refine_Util") structure Eisbach_Rule_Insts: sig end infix 1 ## signature BASIC_REFINE_UTIL = sig val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd val map_fold: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val map_option: ('a -> 'b) -> 'a option -> 'b option val seq_is_empty: 'a Seq.seq -> bool * 'a Seq.seq val split: ('a -> bool) -> 'a list -> 'a list * 'a list val split_matching: ('a -> 'b -> bool) -> 'a list -> 'b list -> ('b list * 'b list) option val yield_singleton2: ('a list -> 'b -> ('c * 'd list) * 'e) -> 'a -> 'b -> ('c * 'd) * 'e end structure Basic_Refine_Util: BASIC_REFINE_UTIL val split_matching = fn: ('a -> 'b -> bool) -> 'a list -> 'b list -> ('b list * 'b list) option val split = fn: ('a -> bool) -> 'a list -> 'a list * 'a list val map_fold = fn: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val yield_singleton2 = fn: ('a list -> 'b -> ('c * 'd list) * 'e) -> 'a -> 'b -> ('c * 'd) * 'e val map_option = fn: ('a -> 'b) -> 'a option -> 'b option val seq_is_empty = fn: 'a Seq.seq -> bool * 'a Seq.seq val ## = fn: ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd ### theory "Automatic_Refinement.Refine_Util_Bootstrap1" ### 0.042s elapsed time, 0.084s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Mk_Term_Antiquot" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib" via "Automatic_Refinement.Refine_Util") val mk_term_antiquot = fn: Context.generic * Token.T list -> string * (Context.generic * Token.T list) ### theory "Automatic_Refinement.Mk_Term_Antiquot" ### 0.159s elapsed time, 0.316s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Mpat_Antiquot" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib" via "Automatic_Refinement.Refine_Util") val mpat_antiquot = fn: Context.generic * Token.T list -> string * (Context.generic * Token.T list) ### theory "Automatic_Refinement.Mpat_Antiquot" ### 0.187s elapsed time, 0.376s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Refine_Util" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") ### ML warning (line 170 of "~~/src/HOL/Eisbach/match_method.ML"): ### Pattern is not exhaustive. ### ML warning (line 187 of "~~/src/HOL/Eisbach/match_method.ML"): ### Pattern is not exhaustive. ### ML warning (line 309 of "~~/src/HOL/Eisbach/match_method.ML"): ### Pattern is not exhaustive. signature MATCH_METHOD = sig val focus_params: Proof.context -> term list val focus_schematics: Proof.context -> Envir.tenv end structure Match_Method: MATCH_METHOD val method_evaluate = fn: Method.text -> Proof.context -> thm list -> tactic ### theory "HOL-Eisbach.Eisbach" ### 0.804s elapsed time, 1.608s cpu time, 0.000s GC time Loading theory "Collections.ICF_Tools" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "Collections.Locale_Code") infix 0 ## signature ICF_TOOLS = sig val changed_conv: conv -> conv val chead_of: cterm -> cterm val chead_of_thm: thm -> cterm val define_simple: string -> term -> local_theory -> (term * thm) * local_theory val define_simple_global: string -> term -> theory -> (term * thm) * theory val define_simple_local: string -> term -> local_theory -> (term * thm) * local_theory val dest_def_eq: term -> term * term val dt_head: term -> term val dt_lhs: term -> term val dt_params: term -> term list val dt_rhs: term -> term val dthm_head: thm -> term val dthm_lhs: thm -> term val dthm_params: thm -> term list val dthm_rhs: thm -> term val gen_variant: (string -> bool) -> string -> string val import_cterm: cterm -> Proof.context -> cterm * Proof.context val inst_meta_cong: Proof.context -> cterm -> thm val map_option: ('a -> 'b) -> 'a option -> 'b option val norm_def_thm: thm -> thm val parse_cpat: cterm context_parser val rem_dup_prems: Proof.context -> thm -> thm val rename_cterm: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val renames_cterm: cterm * cterm -> bool val repeat_top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv val revert_abbrevs: string -> theory -> theory val sss_add: thm list -> Proof.context -> Proof.context val wrap_lthy_global: (local_theory -> local_theory) -> theory -> theory val wrap_lthy_local: (local_theory -> local_theory) -> local_theory -> local_theory val wrap_lthy_result_global: (local_theory -> 'a * local_theory) -> (morphism -> 'a -> 'b) -> theory -> 'b * theory val wrap_lthy_result_local: (local_theory -> 'a * local_theory) -> (morphism -> 'a -> 'b) -> local_theory -> 'b * local_theory end val ## = fn: ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd structure ICF_Tools: ICF_TOOLS ### theory "Collections.ICF_Tools" ### 0.164s elapsed time, 0.424s cpu time, 0.000s GC time Loading theory "Collections.Ord_Code_Preproc" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "Collections.Locale_Code") ### ML warning (line 27 of "~~/afp/thys/Collections/ICF/tools/Ord_Code_Preproc.thy"): ### (=) has infix status but was not preceded by op. ### ML warning (line 38 of "~~/afp/thys/Collections/ICF/tools/Ord_Code_Preproc.thy"): ### Value identifier (trace_ft) has not been referenced. ### ML warning (line 51 of "~~/afp/thys/Collections/ICF/tools/Ord_Code_Preproc.thy"): ### Value identifier (process) has not been referenced. signature ORD_CODE_PREPROC = sig val add: int * string * (theory -> thm -> thm) -> theory -> theory val get: theory -> (int * string * (theory -> thm -> thm)) list val rem: string -> theory -> theory val setup: theory -> theory val trace_enabled: bool ref end signature OC_SIMPSET = sig val get: theory -> simpset val map: (simpset -> simpset) -> theory -> theory val setup: theory -> theory end structure Ord_Code_Preproc: ORD_CODE_PREPROC functor Oc_Simpset (sig val name: string val prio: int end): OC_SIMPSET ### theory "Collections.Ord_Code_Preproc" ### 0.070s elapsed time, 0.140s cpu time, 0.000s GC time Loading theory "Collections.Locale_Code" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform") ### ML warning (line 343 of "~~/afp/thys/Collections/ICF/tools/Locale_Code.thy"): ### Pattern is not exhaustive. signature LOCALE_CODE = sig val add_pat_eq: cterm -> thm list -> theory -> theory val close_block: theory -> theory val del_pat: cterm -> theory -> theory val get_unf_ss: theory -> simpset val lc_decl_del: term -> local_theory -> local_theory val lc_decl_eq: thm list -> local_theory -> local_theory val open_block: theory -> theory type pat_eq = cterm * thm list val setup: theory -> theory val tracing_enabled: bool ref end structure Locale_Code: LOCALE_CODE ### theory "Collections.Locale_Code" ### 0.232s elapsed time, 0.460s cpu time, 0.000s GC time Loading theory "Deriving.Comparator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator" via "Deriving.Comparator_Generator") ### ML warning (line 563 of "~~/afp/thys/Automatic_Refinement/Lib/Refine_Util.thy"): ### Handler catches all exceptions. infix 0 THEN_ELSE' infix 0 THEN_ELSE_COMB' infix 1 THEN_ALL_NEW_FWD infix 1 THEN_INTERVAL infix 2 ORELSE_INTERVAL infix 3 ->> type itactic = int -> int -> tactic type tactic' = int -> tactic signature BASIC_REFINE_UTIL = sig val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd val ->> : 'a context_parser * ('a * Context.generic -> 'b * Context.generic) -> 'b context_parser val ALL_GOALS_FWD: tactic' -> tactic val ALL_GOALS_FWD': tactic' -> tactic' val APPEND_LIST': tactic' list -> tactic' val CAN': tactic' -> tactic' val CASES': (tactic' * tactic) list -> tactic' val CONCL_COND': (term -> bool) -> tactic' val COND': (term -> bool) -> tactic' val IF_EXGOAL: (int -> tactic) -> tactic' val INTERVAL_FWD: tactic' -> int -> int -> tactic val NTIMES': tactic' -> int -> tactic' val ORELSE_INTERVAL: itactic * itactic -> itactic val REPEAT': tactic' -> tactic' val REPEAT_ALL_NEW_FWD: tactic' -> tactic' val REPEAT_DETERM': tactic' -> tactic' val RSm: Proof.context -> thm -> thm -> thm val SINGLE_INTERVAL: itactic -> tactic' val THEN_ALL_NEW_FWD: tactic' * tactic' -> tactic' val THEN_ELSE': tactic' * (tactic' * tactic') -> tactic' val THEN_ELSE_COMB': tactic' * ((tactic' * tactic' -> tactic') * tactic' * tactic') -> tactic' val THEN_INTERVAL: itactic * itactic -> itactic val TRADE: (Proof.context -> tactic') -> Proof.context -> tactic' val TRY_SOLVED': tactic' -> tactic' val WITH_concl: (term -> tactic') -> tactic' val WITH_subgoal: (term -> tactic') -> tactic' val elim_all_tac: Proof.context -> thm list -> tactic val eqsubst_inst_meth: (Proof.context -> Proof.method) context_parser val eqsubst_inst_tac: Proof.context -> bool -> int list -> ((indexname * Position.T) * string) list -> thm -> int -> tactic val fo_resolve_tac: thm list -> Proof.context -> tactic' val fo_rtac: thm -> Proof.context -> tactic' val has_Var: term -> bool val insert_subgoal_tac: cterm -> tactic' val insert_subgoals_tac: cterm list -> tactic' val is_Abs: term -> bool val is_Comb: term -> bool val is_TFree: typ -> bool val is_def_thm: thm -> bool type itactic = int -> int -> tactic val map_fold: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val map_option: ('a -> 'b) -> 'a option -> 'b option val prefer_tac: int -> tactic val rprem_tac: int -> Proof.context -> tactic' val rprems_tac: Proof.context -> tactic' val seq_is_empty: 'a Seq.seq -> bool * 'a Seq.seq val split: ('a -> bool) -> 'a list -> 'a list * 'a list val split_matching: ('a -> 'b -> bool) -> 'a list -> 'b list -> ('b list * 'b list) option type tactic' = int -> tactic val yield_singleton2: ('a list -> 'b -> ('c * 'd list) * 'e) -> 'a -> 'b -> ('c * 'd) * 'e end signature REFINE_UTIL = sig val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd val ->> : 'a context_parser * ('a * Context.generic -> 'b * Context.generic) -> 'b context_parser val ALL_GOALS_FWD: tactic' -> tactic val ALL_GOALS_FWD': tactic' -> tactic' val APPEND_LIST': tactic' list -> tactic' val CAN': tactic' -> tactic' val CASES': (tactic' * tactic) list -> tactic' val CONCL_COND': (term -> bool) -> tactic' val COND': (term -> bool) -> tactic' val HOL_concl_conv: (Proof.context -> conv) -> Proof.context -> conv val IF_EXGOAL: (int -> tactic) -> tactic' val INTERVAL_FWD: tactic' -> int -> int -> tactic val NTIMES': tactic' -> int -> tactic' val OF_fst: thm list -> thm list -> thm val ORELSE_INTERVAL: itactic * itactic -> itactic val REPEAT': tactic' -> tactic' val REPEAT_ALL_NEW_FWD: tactic' -> tactic' val REPEAT_DETERM': tactic' -> tactic' val RS_fst: thm -> thm list -> thm val RSm: Proof.context -> thm -> thm -> thm val SINGLE_INTERVAL: itactic -> tactic' val THEN_ALL_NEW_FWD: tactic' * tactic' -> tactic' val THEN_ELSE': tactic' * (tactic' * tactic') -> tactic' val THEN_ELSE_COMB': tactic' * ((tactic' * tactic' -> tactic') * tactic' * tactic') -> tactic' val THEN_INTERVAL: itactic * itactic -> itactic val TRADE: (Proof.context -> tactic') -> Proof.context -> tactic' val TRY_SOLVED': tactic' -> tactic' val WITH_concl: (term -> tactic') -> tactic' val WITH_subgoal: (term -> tactic') -> tactic' val abs_def: Proof.context -> thm -> thm val anorm_term: term -> term val anorm_typ: typ -> typ val apply_configs: ('a Config.T * 'a) list -> Proof.context -> Proof.context val build_res_net: thm list -> (int * thm) Net.net val cfg_trace_f_tac_conv: bool Config.T val changed_rule: (thm -> thm) -> thm -> thm val dest_itselfT: typ -> typ val dummify_tvars: term -> term val elim_all_tac: Proof.context -> thm list -> tactic val eqsubst_inst_meth: (Proof.context -> Proof.method) context_parser val eqsubst_inst_tac: Proof.context -> bool -> int list -> ((indexname * Position.T) * string) list -> thm -> int -> tactic val f_tac_conv: Proof.context -> (term -> term) -> tactic -> conv val fcomb_conv: conv -> conv val fix_conv: Proof.context -> conv -> conv val fix_left_tuple_from_Ts: string -> typ list -> Proof.context -> term * Proof.context val fixup_vars: cterm -> thm -> thm val fixup_vars_conv: conv -> conv val fixup_vars_conv': (Proof.context -> conv) -> Proof.context -> conv val fo_matches: theory -> cterm -> term -> bool val fo_matchp: theory -> cterm -> term -> term list option val fo_resolve_tac: thm list -> Proof.context -> tactic' val fo_rtac: thm -> Proof.context -> tactic' val fold_binop_left: ('a -> 'b * 'a) -> ('c -> 'a -> 'b * 'a) -> ('b * 'b -> 'b) -> 'c list -> 'a -> 'b * 'a val fsub_conv: (Proof.context -> conv) -> Proof.context -> conv val ftop_conv: (Proof.context -> conv) -> Proof.context -> conv val has_Var: term -> bool val import_conv: (Proof.context -> conv) -> Proof.context -> conv val import_cterms: bool -> cterm list -> Proof.context -> cterm list * Proof.context val insert_subgoal_tac: cterm -> tactic' val insert_subgoals_tac: cterm list -> tactic' val instantiate_tuples: Proof.context -> (indexname * typ) list -> thm -> thm val instantiate_tuples_from_term_tac: Proof.context -> term -> tactic val instantiate_tuples_subgoal_tac: Proof.context -> tactic' val is_Abs: term -> bool val is_Comb: term -> bool val is_TFree: typ -> bool val is_def_thm: thm -> bool type itactic = int -> int -> tactic val ite_conv: conv -> conv -> conv -> conv val lambda_tuple: term list -> term -> term val list_binop_left: 'a -> ('a * 'a -> 'a) -> 'a list -> 'a val list_prodT_left: typ list -> typ val map_fold: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val map_option: ('a -> 'b) -> 'a option -> 'b option val mk_compN: int -> term -> term -> term val mk_compN1: typ list -> int -> term -> term -> term val mk_ltuple: term list -> term val monitor_conv: string -> conv -> conv val monitor_conv': string -> (Proof.context -> conv) -> Proof.context -> conv val order_by: ('a * 'a -> order) -> ('b -> 'a) -> 'b list -> 'b list val parse_bool_config: string -> bool Config.T -> bool context_parser val parse_bool_config': string -> bool Config.T -> Token.T list -> (bool Config.T * bool) * Token.T list val parse_paren_list: 'a context_parser -> 'a list context_parser val parse_paren_list': 'a parser -> Token.T list -> 'a list * Token.T list val parse_paren_lists: 'a context_parser -> 'a list list context_parser val pat_conv: cterm -> (Proof.context -> conv) -> Proof.context -> conv val pat_conv': cterm -> (string -> Proof.context -> conv) -> Proof.context -> conv val prefer_tac: int -> tactic val repeat_rule: (thm -> thm) -> thm -> thm val rprem_tac: int -> Proof.context -> tactic' val rprems_tac: Proof.context -> tactic' val seq_is_empty: 'a Seq.seq -> bool * 'a Seq.seq val shift_lambda_left: thm -> thm val shift_lambda_leftN: int -> thm -> thm val split: ('a -> bool) -> 'a list -> 'a list * 'a list val split_matching: ('a -> 'b -> bool) -> 'a list -> 'b list -> ('b list * 'b list) option val strip_prodT_left: typ -> typ list val subsume_sort: ('a -> term) -> theory -> 'a list -> 'a list val subsume_sort_gen: ('a -> term) -> Context.generic -> 'a list -> 'a list type tactic' = int -> tactic val trace_conv: conv val trade_rule: (Proof.context -> thm -> thm) -> Proof.context -> thm -> thm val try_rule: (thm -> thm) -> thm -> thm val yield_singleton2: ('a list -> 'b -> ('c * 'd list) * 'e) -> 'a -> 'b -> ('c * 'd) * 'e end structure Refine_Util: REFINE_UTIL structure Basic_Refine_Util: BASIC_REFINE_UTIL val ORELSE_INTERVAL = fn: itactic * itactic -> itactic val split = fn: ('a -> bool) -> 'a list -> 'a list * 'a list val fo_resolve_tac = fn: thm list -> Proof.context -> tactic' val RSm = fn: Proof.context -> thm -> thm -> thm val prefer_tac = fn: int -> tactic val WITH_subgoal = fn: (term -> tactic') -> tactic' val NTIMES' = fn: tactic' -> int -> tactic' val map_option = fn: ('a -> 'b) -> 'a option -> 'b option val REPEAT_DETERM' = fn: tactic' -> tactic' val THEN_ELSE_COMB' = fn: tactic' * ((tactic' * tactic' -> tactic') * tactic' * tactic') -> tactic' val SINGLE_INTERVAL = fn: itactic -> tactic' val insert_subgoals_tac = fn: cterm list -> tactic' val ALL_GOALS_FWD' = fn: tactic' -> tactic' val yield_singleton2 = fn: ('a list -> 'b -> ('c * 'd list) * 'e) -> 'a -> 'b -> ('c * 'd) * 'e val insert_subgoal_tac = fn: cterm -> tactic' val INTERVAL_FWD = fn: tactic' -> int -> int -> tactic val split_matching = fn: ('a -> 'b -> bool) -> 'a list -> 'b list -> ('b list * 'b list) option val IF_EXGOAL = fn: (int -> tactic) -> tactic' val seq_is_empty = fn: 'a Seq.seq -> bool * 'a Seq.seq val elim_all_tac = fn: Proof.context -> thm list -> tactic val TRADE = fn: (Proof.context -> tactic') -> Proof.context -> tactic' val APPEND_LIST' = fn: tactic' list -> tactic' val is_TFree = fn: typ -> bool val ## = fn: ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd val CAN' = fn: tactic' -> tactic' val fo_rtac = fn: thm -> Proof.context -> tactic' val is_Abs = fn: term -> bool val COND' = fn: (term -> bool) -> tactic' val CONCL_COND' = fn: (term -> bool) -> tactic' val CASES' = fn: (tactic' * tactic) list -> tactic' val map_fold = fn: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val THEN_ALL_NEW_FWD = fn: tactic' * tactic' -> tactic' val WITH_concl = fn: (term -> tactic') -> tactic' val is_Comb = fn: term -> bool val eqsubst_inst_tac = fn: Proof.context -> bool -> int list -> ((indexname * Position.T) * string) list -> thm -> int -> tactic val eqsubst_inst_meth = fn: (Proof.context -> Proof.method) context_parser val ->> = fn: 'a context_parser * ('a * Context.generic -> 'b * Context.generic) -> 'b context_parser val ALL_GOALS_FWD = fn: tactic' -> tactic val is_def_thm = fn: thm -> bool val THEN_INTERVAL = fn: itactic * itactic -> itactic val rprem_tac = fn: int -> Proof.context -> tactic' val rprems_tac = fn: Proof.context -> tactic' val has_Var = fn: term -> bool val REPEAT' = fn: tactic' -> tactic' val THEN_ELSE' = fn: tactic' * (tactic' * tactic') -> tactic' val TRY_SOLVED' = fn: tactic' -> tactic' val REPEAT_ALL_NEW_FWD = fn: tactic' -> tactic' ### theory "Automatic_Refinement.Refine_Util" ### 0.668s elapsed time, 1.436s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Anti_Unification" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature ANTI_UNIFICATION = sig val anti_unify: term * term -> term val anti_unifyT: typ * typ -> typ_env -> typ * typ_env val anti_unify_env: term * term -> env -> term * env val anti_unify_list: term list -> term val empty: env val empty_term: term_env val empty_typ: typ_env type env = typ_env * term_env val specialize_net_tac: Proof.context -> (int * thm) Net.net -> tactic' val specialize_tac: Proof.context -> thm list -> tactic' type term_env type typ_env end structure Anti_Unification: ANTI_UNIFICATION ### theory "Automatic_Refinement.Anti_Unification" ### 0.122s elapsed time, 0.244s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Attr_Comb" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") infixr 5 THEN_ATTR infixr 4 ELSE_ATTR signature ATTR_COMB = sig exception ATTR_EXC of string val CHECK_PREPARE: (Context.generic * thm -> bool) -> attribute -> attribute val COND_attr: (Context.generic * thm -> bool) -> attribute val EFF_ATTR: (Context.generic * thm -> 'a) -> attribute val ELSE_ATTR: attribute * attribute -> attribute val ID_ATTR: attribute val IGNORE_THM: attribute -> attribute val ITE_ATTR: attribute -> attribute -> attribute -> attribute val ITE_ATTR': attribute -> attribute -> (exn -> attribute) -> attribute val NO_ATTR: attribute val RPT1_ATTR: attribute -> attribute val RPT_ATTR: attribute -> attribute val RS_attr: thm -> attribute val RSm_attr: thm -> attribute val THEN_ATTR: attribute * attribute -> attribute val TRACE_ATTR: string -> attribute -> attribute val TRY_ATTR: attribute -> attribute val WARN_ATTR: Context.generic -> string -> attribute end structure Attr_Comb: ATTR_COMB ### theory "Automatic_Refinement.Attr_Comb" ### 0.085s elapsed time, 0.168s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Named_Sorted_Thms" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature NAMED_SORTED_THMS = sig val add: attribute val add_thm: thm -> Context.generic -> Context.generic val del: attribute val del_thm: thm -> Context.generic -> Context.generic val get: Proof.context -> thm list val member: Proof.context -> thm -> bool val setup: theory -> theory end functor Named_Sorted_Thms ( sig val description: string val name: binding val sort: Context.generic -> thm list -> thm list val transform: Context.generic -> thm -> thm list end ): NAMED_SORTED_THMS ### theory "Automatic_Refinement.Named_Sorted_Thms" ### 0.041s elapsed time, 0.084s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Autoref_Data" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops") signature AUTOREF_DATA = sig type T exception exCIRCULAR exception exNULL val get: Proof.context -> T val init: Proof.context -> Proof.context end functor Autoref_Data ( sig type T val compute: Proof.context -> T val prereq: (Proof.context -> Proof.context) list end ): AUTOREF_DATA ### theory "Automatic_Refinement.Autoref_Data" ### 0.175s elapsed time, 0.276s cpu time, 0.212s GC time Loading theory "Automatic_Refinement.Indep_Vars" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature INDEP_VARS = sig val indep_tac: Proof.context -> tactic' end structure Indep_Vars: INDEP_VARS ### theory "Automatic_Refinement.Indep_Vars" ### 0.052s elapsed time, 0.104s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Mk_Record_Simp" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") val mk_record_simp = fn: Context.generic -> thm -> thm ### theory "Automatic_Refinement.Mk_Record_Simp" ### 0.042s elapsed time, 0.088s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Tagged_Solver" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature TAGGED_SOLVER = sig val add_triggers: string -> thm list -> morphism -> Context.generic -> Context.generic val cfg_full: bool Config.T val cfg_keep: bool Config.T val cfg_step: bool Config.T val cfg_trace: bool Config.T val declare_solver: thm list -> binding -> string -> (Proof.context -> tactic') -> morphism -> Context.generic -> Context.generic val delete_solver: string -> morphism -> Context.generic -> Context.generic val get_potential_solvers: Proof.context -> int -> thm -> solver list val get_potential_tacs: Proof.context -> int -> thm -> tactic' list val get_solvers: Proof.context -> solver list val lookup_solver: string -> Context.generic -> solver option val pretty_solvers: Proof.context -> Pretty.T val solve_full_keep_tac: Proof.context -> tactic' val solve_full_step_tac: Proof.context -> tactic' val solve_full_tac: Proof.context -> tactic' val solve_greedy_keep_tac: Proof.context -> tactic' val solve_greedy_step_tac: Proof.context -> tactic' val solve_greedy_tac: Proof.context -> tactic' val solve_tac: Proof.context -> tactic' type solver = thm list * string * string * (Proof.context -> tactic') val tac_of_solver: Proof.context -> solver -> tactic' end structure Tagged_Solver: TAGGED_SOLVER ### theory "Automatic_Refinement.Tagged_Solver" ### 0.113s elapsed time, 0.228s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Select_Solve" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") signature SELECT_SOLVE = sig val AS_FIRSTGOAL: tactic -> tactic' val IF_SUBGOAL_SOLVED: tactic -> tactic -> tactic -> tactic val PREFER_SOLVED: tactic -> tactic val REPEAT_SOLVE_FWD_SELECT: Proof.context -> int -> tactic' -> tactic' val SELECT_FIRST: Proof.context -> tactic -> tactic val TRY_SOLVE_FWD: int -> tactic -> tactic end structure Select_Solve: SELECT_SOLVE ### theory "Automatic_Refinement.Select_Solve" ### 0.074s elapsed time, 0.148s cpu time, 0.000s GC time Loading theory "Deriving.Derive_Manager" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator" via "Deriving.Comparator_Generator") signature DERIVE_MANAGER = sig val derive: string -> string -> string -> theory -> theory val derive_cmd: string -> string -> string -> theory -> theory val print_info: theory -> unit val register_derive: string -> string -> (string -> string -> theory -> theory) -> theory -> theory end structure Derive_Manager: DERIVE_MANAGER ### theory "Deriving.Derive_Manager" ### 0.053s elapsed time, 0.108s cpu time, 0.000s GC time Loading theory "Deriving.Generator_Aux" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator" via "Deriving.Comparator_Generator") Found termination order: "{}" locale comparator fixes comp :: "'a \ 'a \ order" assumes "comparator comp" signature BNF_ACCESS = sig val bnf_types: Proof.context -> string list -> typ list val case_consts: Proof.context -> string list -> term list val case_simps: Proof.context -> string list -> thm list list val case_thms: Proof.context -> string list -> thm list val constr_argument_types: Proof.context -> string list -> typ list list list val constr_terms: Proof.context -> string -> term list val distinct_thms: Proof.context -> string list -> thm list list val induct_thms: Proof.context -> string list -> thm list val inject_thms: Proof.context -> string list -> thm list list val map_comps: Proof.context -> string list -> thm list val map_simps: Proof.context -> string list -> thm list list val map_terms: Proof.context -> string list -> term list val set_simps: Proof.context -> string list -> thm list list val set_terms: Proof.context -> string list -> term list list end structure Bnf_Access: BNF_ACCESS signature GENERATOR_AUX = sig val OF_option: thm -> thm option list -> thm val add_used_tycos: Proof.context -> string -> string list -> string list val alist_to_string: (string * 'a) list -> string val conjI_tac: thm list -> Proof.context -> 'a list -> (Proof.context -> int -> tactic) -> tactic val create_map: (typ -> term) -> (string * typ -> 'a -> term) -> 'a -> (typ -> bool) -> (local_theory -> string -> bool list) -> (local_theory -> string -> term) -> (local_theory -> string -> 'a -> term) -> string list -> (local_theory -> string -> 'a) -> typ -> local_theory -> term val create_partial: 'a -> (typ -> bool) -> (local_theory -> string -> bool list) -> (local_theory -> string -> term) -> (local_theory -> string -> 'a -> term) -> string list -> (local_theory -> string -> 'a) -> typ -> local_theory -> term val define_overloaded: string * term -> local_theory -> thm * local_theory val define_overloaded_generic: Attrib.binding * term -> local_theory -> thm * local_theory val drop_last: 'a list -> 'a list val freeify_tvars: typ -> typ val ind_case_to_idxs: 'a list list -> int -> int * int val infer_type: Proof.context -> term -> term val ints_to_subscript: int list -> string val is_class_instance: theory -> string -> sort -> bool val lambdas: term list -> term -> term val mk_case_tac: Proof.context -> term option list list -> thm -> (int -> Proof.context * thm list * (string * cterm) list -> tactic) -> tactic val mk_def: typ -> string -> term -> term val mk_id: typ -> term val mk_infer_const: string -> Proof.context -> term -> term val mutual_recursive_types: string -> Proof.context -> string list * typ list val prove_multi_future: Proof.context -> string list -> term list -> term list -> ({context: Proof.context, prems: thm list} -> tactic) -> thm list val recursor: (string -> 'a) * ('a -> bool list) * string list -> bool -> (typ -> 'b) -> (typ -> 'b) -> (typ -> 'b) -> ((typ * 'b option) list * 'a -> 'b) -> typ -> 'b val rename_types: (typ * typ) list -> term -> term val restore_with_morphism: local_theory -> morphism * local_theory val split_IHs: (string -> 'a) * ('a -> bool list) * string list -> typ list -> thm list -> thm list list val std_recursor_tac: (string -> 'a) * ('a -> bool list) * string list -> typ list -> ('a -> thm) -> thm list -> typ -> thm list -> Proof.context -> tactic val sub: string -> string val subT: string -> typ -> string val typ_and_vs_of_typname: theory -> string -> sort -> typ * (string * sort) list val typ_and_vs_of_used_typname: string -> bool list -> string list -> typ * (string * string list) list val type_parameters: typ -> Proof.context -> (string * sort) list * typ list end structure Generator_Aux: GENERATOR_AUX ### theory "Deriving.Generator_Aux" ### 0.184s elapsed time, 0.368s cpu time, 0.000s GC time Loading theory "Deriving.Equality_Generator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Equality_Instances") ### theory "Deriving.Comparator" ### 1.138s elapsed time, 2.200s cpu time, 0.212s GC time Loading theory "Deriving.Compare" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator") class compare = type + fixes compare :: "'a \ 'a \ order" assumes "comparator_compare": "comparator compare" class compare_order = compare + ord + assumes "ord_defs": "le_of_comp compare = (\)" "lt_of_comp compare = (<)" signature EQUALITY_GENERATOR = sig val ensure_info: equality_type -> string -> local_theory -> local_theory datatype equality_type = BNF | EQ val generate_equality: equality_type -> string -> local_theory -> local_theory val generate_equalitys_from_bnf_fp: string -> local_theory -> ((term * thm list) list * (term * thm) list) * local_theory val get_info: Proof.context -> string -> info option type info = {equality: term, equality_def: thm option, equality_thm: thm, map: term, map_comp: thm option, partial_equality_thm: thm, pequality: term, used_positions: bool list} val register_equality_of: string -> local_theory -> local_theory val register_foreign_equality: typ -> term -> thm -> local_theory -> local_theory val register_foreign_partial_and_full_equality: string -> term -> term -> term -> thm option -> thm option -> thm -> thm -> bool list -> local_theory -> local_theory end structure Equality_Generator: EQUALITY_GENERATOR ### theory "Deriving.Equality_Generator" ### 0.349s elapsed time, 0.700s cpu time, 0.000s GC time Loading theory "Deriving.Comparator_Generator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator") class compare_order = compare + linorder + assumes "ord_defs": "le_of_comp compare = (\)" "lt_of_comp compare = (<)" signature COMPARE_CODE = sig val change_compare_code: term -> string list -> local_theory -> local_theory end structure Compare_Code: COMPARE_CODE ### theory "Deriving.Compare" ### 0.525s elapsed time, 1.052s cpu time, 0.000s GC time Loading theory "Deriving.Equality_Instances" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive") generating equality for type "Sum_Type.sum" generating equality for type "List.list" generating equality for type "Product_Type.prod" Found termination order: "size_list size <*mlex*> {}" generating equality for type "Option.option" ### theory "Deriving.Equality_Instances" ### 0.111s elapsed time, 0.220s cpu time, 0.000s GC time Loading theory "HOL-Library.AList" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "HOL-ODE-Numerics.GenCF_No_Comp" via "Collections.Impl_Array_Map" via "Collections.Diff_Array" via "Collections.Assoc_List") consts update :: "'key \ 'val \ ('key \ 'val) list \ ('key \ 'val) list" consts update_with_aux :: "'val \ 'key \ ('val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" signature COMPARATOR_GENERATOR = sig datatype comparator_type = BNF | Linorder val ensure_info: comparator_type -> string -> local_theory -> local_theory val generate_comparator: comparator_type -> string -> local_theory -> local_theory val generate_comparators_from_bnf_fp: string -> local_theory -> ((term * thm list) list * (term * thm) list) * local_theory val get_info: Proof.context -> string -> info option type info = {comp: term, comp_def: thm option, comp_thm: thm, map: term, map_comp: thm option, partial_comp_thms: thm list, pcomp: term, used_positions: bool list} val register_comparator_of: string -> local_theory -> local_theory val register_foreign_comparator: typ -> term -> thm -> local_theory -> local_theory val register_foreign_partial_and_full_comparator: string -> term -> term -> term -> thm option -> thm option -> thm -> thm -> thm -> thm -> bool list -> local_theory -> local_theory end structure Comparator_Generator: COMPARATOR_GENERATOR ### theory "Deriving.Comparator_Generator" ### 0.838s elapsed time, 1.684s cpu time, 0.000s GC time Loading theory "Deriving.Compare_Generator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances") Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" signature COMPARE_GENERATOR = sig val compare_instance: Comparator_Generator.comparator_type -> string -> theory -> theory val compare_order_instance_via_comparator_of: string -> theory -> theory val compare_order_instance_via_compare: string -> theory -> theory end structure Compare_Generator: COMPARE_GENERATOR ### theory "Deriving.Compare_Generator" ### 0.454s elapsed time, 0.900s cpu time, 0.000s GC time Loading theory "HOL-Library.Adhoc_Overloading" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "HOL-Library.Monad_Syntax") 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.118s elapsed time, 0.236s cpu time, 0.000s GC time Loading theory "HOL-Library.Monad_Syntax" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation") ### theory "HOL-Library.Monad_Syntax" ### 0.059s elapsed time, 0.112s cpu time, 0.000s GC time Loading theory "HOL-Library.Bit" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word" via "HOL-Word.Bits_Bit") instantiation bit :: {one,zero} zero_bit == zero_class.zero :: bit one_bit == one_class.one :: bit Proofs for inductive predicate(s) "rec_set_bit" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the simplification rules ... instantiation bit :: field inverse_bit == inverse :: bit \ bit divide_bit == divide :: bit \ bit \ bit uminus_bit == uminus :: bit \ bit minus_bit == minus :: bit \ bit \ bit times_bit == times :: bit \ bit \ bit plus_bit == plus :: bit \ bit \ bit Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" class zero_neq_one = one + zero + assumes "zero_neq_one": "(0::'a) \ (1::'a)" ### theory "HOL-Library.Bit" ### 0.560s elapsed time, 1.108s cpu time, 0.000s GC time Loading theory "HOL-Library.Boolean_Algebra" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word") locale boolean fixes conj :: "'a \ 'a \ 'a" (infixr "\" 70) and disj :: "'a \ 'a \ 'a" (infixr "\" 65) and compl :: "'a \ 'a" ("\ _" [81] 80) and zero :: "'a" ("\") and one :: "'a" ("\") assumes "boolean (\) (\) compl \ \" Found termination order: "(\p. size_list size (snd (snd (snd p)))) <*mlex*> {}" ### theory "HOL-Library.AList" ### 1.794s elapsed time, 3.568s cpu time, 0.000s GC time Loading theory "HOL-Library.Permutation" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Affine_Form") Proofs for inductive predicate(s) "perm" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale boolean_xor fixes conj :: "'a \ 'a \ 'a" (infixr "\" 70) and disj :: "'a \ 'a \ 'a" (infixr "\" 65) and compl :: "'a \ 'a" ("\ _" [81] 80) and zero :: "'a" ("\") and one :: "'a" ("\") and xor :: "'a \ 'a \ 'a" (infixr "\" 65) assumes "boolean_xor (\) (\) compl \ \ (\)" ### theory "HOL-Library.Boolean_Algebra" ### 0.657s elapsed time, 1.244s cpu time, 0.668s GC time Loading theory "HOL-ex.Quicksort" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib" via "Automatic_Refinement.Misc") ### Ignoring duplicate safe introduction (intro!) ### ?xs <~~> ?ys \ ?z # ?xs <~~> ?z # ?ys ### Ignoring duplicate safe introduction (intro!) ### ?xs <~~> ?ys \ ?z # ?xs <~~> ?z # ?ys ### theory "HOL-Library.Permutation" ### 0.551s elapsed time, 1.040s cpu time, 0.668s GC time Loading theory "HOL-Library.Char_ord" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Compare_Instances") instantiation char :: linorder less_eq_char == less_eq :: char \ char \ bool less_char == less :: char \ char \ bool class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" instantiation char :: distrib_lattice inf_char == inf :: char \ char \ char sup_char == sup :: char \ char \ char ### theory "HOL-Library.Char_ord" ### 0.093s elapsed time, 0.184s cpu time, 0.000s GC time Loading theory "Deriving.Compare_Instances" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive") deriving "compare_order" instance for type "Int.int" deriving "compare" instance for type "Int.int" deriving "compare_order" instance for type "Code_Numeral.integer" deriving "compare" instance for type "Code_Numeral.integer" deriving "compare_order" instance for type "Nat.nat" deriving "compare" instance for type "Nat.nat" Found termination order: "length <*mlex*> {}" deriving "compare_order" instance for type "String.char" deriving "compare" instance for type "String.char" deriving "compare" instance for type "Sum_Type.sum" generating comparator for type "Sum_Type.sum" deriving "compare" instance for type "List.list" generating comparator for type "List.list" ### theory "HOL-ex.Quicksort" ### 0.496s elapsed time, 0.968s cpu time, 0.000s GC time Loading theory "HOL-Library.Mapping" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation") deriving "compare" instance for type "Product_Type.prod" generating comparator for type "Product_Type.prod" deriving "compare" instance for type "Option.option" generating comparator for type "Option.option" Found termination order: "{}" Found termination order: "{}" deriving "compare" instance for type "HOL.bool" deriving "compare" instance for type "Product_Type.unit" deriving "compare_order" instance for type "HOL.bool" deriving "compare_order" instance for type "Product_Type.unit" ### theory "Deriving.Compare_Instances" ### 0.665s elapsed time, 1.264s cpu time, 0.000s GC time Loading theory "HOL-Library.Option_ord" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib" via "Automatic_Refinement.Misc") ### Not an abstract type: Mapping.mapping, in theorem: ### lookup (Mapping ?f) \ ?f instantiation option :: (preorder) preorder less_eq_option == less_eq :: 'a option \ 'a option \ bool less_option == less :: 'a option \ 'a option \ bool instantiation option :: (order) order_bot bot_option == bot :: 'a option instantiation option :: (order_top) order_top top_option == top :: 'a option instantiation option :: (inf) inf inf_option == inf :: 'a option \ 'a option \ 'a option instantiation option :: (sup) sup sup_option == sup :: 'a option \ 'a option \ 'a option instantiation option :: (complete_lattice) complete_lattice Inf_option == Inf :: 'a option set \ 'a option Sup_option == Sup :: 'a option set \ 'a option instantiation mapping :: (type, type) equal equal_mapping == equal_class.equal :: ('a, 'b) mapping \ ('a, 'b) mapping \ bool ### theory "HOL-Library.Option_ord" ### 0.429s elapsed time, 0.860s cpu time, 0.000s GC time Loading theory "Automatic_Refinement.Misc" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_Basic" via "Refine_Monadic.Refine_Misc" via "Automatic_Refinement.Automatic_Refinement" via "Automatic_Refinement.Autoref_Tool" via "Automatic_Refinement.Autoref_Translate" via "Automatic_Refinement.Autoref_Fix_Rel" via "Automatic_Refinement.Autoref_Id_Ops" via "Automatic_Refinement.Refine_Lib") locale combine_mapping_abel_semigroup fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) assumes "combine_mapping_abel_semigroup (\<^bold>* )" ### theory "HOL-Library.Mapping" ### 1.187s elapsed time, 2.348s cpu time, 0.000s GC time Loading theory "HOL-Library.Parallel" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics") ### theory "Automatic_Refinement.Misc" ### 0.767s elapsed time, 1.508s cpu time, 0.000s GC time Loading theory "HOL-Library.Type_Length" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word") class len0 = type + fixes len_of :: "'a itself \ nat" class len = len0 + assumes "len_gt_0": "0 < LENGTH('a)" instantiation 0 :: len0 1 :: len0 len_of_num0 == len_of :: 0 itself \ nat len_of_num1 == len_of :: 1 itself \ nat instantiation bit0 :: (len0) len0 bit1 :: (len0) len0 len_of_bit0 == len_of :: 'a bit0 itself \ nat len_of_bit1 == len_of :: 'a bit1 itself \ nat ### theory "HOL-Library.Type_Length" ### 0.147s elapsed time, 0.280s cpu time, 0.000s GC time Loading theory "HOL-Library.RBT_Impl" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "HOL-Library.RBT_Mapping" via "HOL-Library.RBT") consts join :: "'a future \ 'a" ### theory "HOL-Library.Parallel" ### 0.726s elapsed time, 1.396s cpu time, 0.000s GC time Loading theory "HOL-Library.While_Combinator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic" via "Refine_Monadic.Refine_While" via "Refine_Monadic.RefineG_While") Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" ### theory "HOL-Library.While_Combinator" ### 1.079s elapsed time, 1.956s cpu time, 0.624s GC time Loading theory "HOL-Types_To_Sets.Types_To_Sets" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform") signature LOCAL_TYPEDEF = sig val cancel_type_definition: thm -> thm val cancel_type_definition_attr: attribute end structure Local_Typedef: LOCAL_TYPEDEF signature UNOVERLOADING = sig val unoverload: cterm -> thm -> thm val unoverload_attr: cterm -> attribute end structure Unoverloading: UNOVERLOADING signature INTERNALIZE_SORT = sig val internalize_sort: ctyp -> thm -> typ * thm val internalize_sort_attr: typ -> attribute end structure Internalize_Sort: INTERNALIZE_SORT signature UNOVERLOAD_TYPE = sig val unoverload_type: Context.generic -> indexname list -> thm -> thm val unoverload_type_attr: indexname list -> attribute end structure Unoverload_Type: UNOVERLOAD_TYPE ### theory "HOL-Types_To_Sets.Types_To_Sets" ### 0.147s elapsed time, 0.296s cpu time, 0.000s GC time Loading theory "HOL-Word.Bits_Bit" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word") instantiation bit :: bit bitNOT_bit == bitNOT :: bit \ bit bitAND_bit == bitAND :: bit \ bit \ bit bitOR_bit == bitOR :: bit \ bit \ bit bitXOR_bit == bitXOR :: bit \ bit \ bit consts bitNOT_bit :: "bit \ bit" consts bitAND_bit :: "bit \ bit \ bit" consts bitOR_bit :: "bit \ bit \ bit" consts bitXOR_bit :: "bit \ bit \ bit" ### theory "HOL-Word.Bits_Bit" ### 0.299s elapsed time, 0.600s cpu time, 0.000s GC time Loading theory "Native_Word.More_Bits_Int" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc") consts bin_mask :: "nat \ int" consts entries :: "('a, 'b) rbt \ ('a \ 'b) list" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" consts rbt_sorted :: "('a, 'b) rbt \ bool" Found termination order: "(\p. size (snd p)) <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" consts rbt_lookup :: "('a, 'b) rbt \ 'a \ 'b option" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" Found termination order: "(\p. size (snd p)) <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" consts color_of :: "('a, 'b) rbt \ color" consts bheight :: "('a, 'b) rbt \ nat" consts inv1 :: "('a, 'b) rbt \ bool" consts inv1l :: "('a, 'b) rbt \ bool" consts inv2 :: "('a, 'b) rbt \ bool" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" 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 ... ### theory "Native_Word.More_Bits_Int" ### 1.950s elapsed time, 3.908s cpu time, 0.000s GC time Loading theory "Native_Word.Bits_Integer" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32") 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 Found termination order: "(nat \ abs) <*mlex*> {}" 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 File "ROOT.ocaml", line 287, characters 32-33: Warning 20: this argument will not be used by the function. File "ROOT.ocaml", line 287, characters 34-35: Warning 20: this argument will not be used by the function. File "ROOT.ocaml", line 287, characters 36-37: Warning 20: this argument will not be used by the function. Found termination order: "{}" ### Ignoring duplicate rewrite rule: ### balance Empty ?s1 ?t1 Empty \ Branch B Empty ?s1 ?t1 Empty ### Ignoring duplicate rewrite rule: ### balance (Branch B ?va1 ?vb1 ?vc1 ?vd1) ?s1 ?t1 Empty \ ### Branch B (Branch B ?va1 ?vb1 ?vc1 ?vd1) ?s1 ?t1 Empty ### Ignoring duplicate rewrite rule: ### balance Empty ?s1 ?t1 (Branch B ?va1 ?vb1 ?vc1 ?vd1) \ ### Branch B Empty ?s1 ?t1 (Branch B ?va1 ?vb1 ?vc1 ?vd1) class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" consts paint :: "color \ ('a, 'b) rbt \ ('a, 'b) rbt" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" Found termination order: "(\p. size (snd (snd (snd p)))) <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "Native_Word.Bits_Integer" ### 14.480s elapsed time, 17.104s cpu time, 0.756s GC time Loading theory "Native_Word.Code_Target_Bits_Int" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "HOL-ODE-Numerics.GenCF_No_Comp" via "Collections.Impl_Array_Hash_Map" via "Collections.Intf_Hash" via "Collections.Code_Target_ICF") ### theory "Native_Word.Code_Target_Bits_Int" ### 0.234s elapsed time, 0.468s cpu time, 0.000s GC time Loading theory "Collections.Code_Target_ICF" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "HOL-ODE-Numerics.GenCF_No_Comp" via "Collections.Impl_Array_Hash_Map" via "Collections.Intf_Hash") Found termination order: "{}" ### theory "Collections.Code_Target_ICF" ### 0.231s elapsed time, 0.464s cpu time, 0.000s GC time Loading theory "HOL-Word.Word_Miscellaneous" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word") class order = preorder + assumes "antisym": "\x y. \x \ y; y \ x\ \ x = y" ### theory "HOL-Word.Word_Miscellaneous" ### 0.430s elapsed time, 0.860s cpu time, 0.000s GC time Loading theory "HOL-Word.Misc_Typedef" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word") locale type_definition fixes Rep :: "'b \ 'a" and Abs :: "'a \ 'b" and A :: "'a set" assumes "type_definition Rep Abs A" locale td_ext fixes Rep :: "'a \ 'b" and Abs :: "'b \ 'a" and A :: "'b set" and norm :: "'b \ 'b" assumes "td_ext Rep Abs A norm" ### theory "HOL-Word.Misc_Typedef" ### 0.173s elapsed time, 0.348s cpu time, 0.000s GC time Loading theory "HOL-Word.Word" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc") Found termination order: "{}" class order = preorder + assumes "antisym": "\x y. \x \ y; y \ x\ \ x = y" Found termination order: "(\p. size (snd p)) <*mlex*> (\p. size (fst p)) <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" instantiation word :: (len0) size size_word == size :: 'a word \ nat instantiation word :: (len0) equal equal_word == equal_class.equal :: 'a word \ 'a word \ bool instantiation word :: ({len0,typerep}) random random_word == random_class.random :: natural \ natural \ natural \ ('a word \ (unit \ term)) \ natural \ natural instantiation word :: (len0) {comm_monoid_mult,neg_numeral,comm_ring,modulo} modulo_word == modulo :: 'a word \ 'a word \ 'a word divide_word == divide :: 'a word \ 'a word \ 'a word minus_word == minus :: 'a word \ 'a word \ 'a word uminus_word == uminus :: 'a word \ 'a word zero_word == zero_class.zero :: 'a word plus_word == plus :: 'a word \ 'a word \ 'a word one_word == one_class.one :: 'a word times_word == times :: 'a word \ 'a word \ 'a word instantiation word :: (len0) linorder less_eq_word == less_eq :: 'a word \ 'a word \ bool less_word == less :: 'a word \ 'a word \ bool instantiation word :: (len0) bits test_bit_word == test_bit :: 'a word \ nat \ bool lsb_word == lsb :: 'a word \ bool set_bit_word == set_bit :: 'a word \ nat \ bool \ 'a word set_bits_word == set_bits :: (nat \ bool) \ 'a word shiftl_word == shiftl :: 'a word \ nat \ 'a word shiftr_word == shiftr :: 'a word \ nat \ 'a word bitNOT_word == bitNOT :: 'a word \ 'a word bitAND_word == bitAND :: 'a word \ 'a word \ 'a word bitOR_word == bitOR :: 'a word \ 'a word \ 'a word bitXOR_word == bitXOR :: 'a word \ 'a word \ 'a word instantiation word :: (len) bitss msb_word == msb :: 'a word \ bool ### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem: ### linorder.Min word_sle (set (?x # ?xs)) \ fold signed.min ?xs ?x ### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem: ### linorder.Max word_sle (set (?x # ?xs)) \ fold signed.max ?xs ?x ### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem: ### signed.sorted [] \ True ### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem: ### signed.sorted [?x] \ True ### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem: ### signed.sorted (?x # ?y # ?zs) \ ### ?x <=s ?y \ signed.sorted (?y # ?zs) ### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem: ### signed.sorted_list_of_set (set ?xs) \ signed.sort (remdups ?xs) val uint_arith_simpset = fn: Proof.context -> Proof.context val uint_arith_tacs = fn: Proof.context -> tactic list val uint_arith_tac = fn: Proof.context -> int -> tactic val unat_arith_simpset = fn: Proof.context -> Proof.context val unat_arith_tacs = fn: Proof.context -> tactic list val unat_arith_tac = fn: Proof.context -> int -> tactic ### Ignoring duplicate rewrite rule: ### ?y AND - 1 \ ?y ### Ignoring duplicate rewrite rule: ### ?x1 OR - 1 \ - 1 ### Ignoring duplicate rewrite rule: ### ?x1 XOR - 1 \ NOT ?x1 ### Ignoring duplicate rewrite rule: ### - 1 AND ?y \ ?y ### Ignoring duplicate rewrite rule: ### - 1 OR ?x1 \ - 1 ### Ignoring duplicate rewrite rule: ### - 1 XOR ?x1 \ NOT ?x1 locale word_rotate Found termination order: "case_sum (\p. size (fst (snd p))) (case_sum (\p. size (snd (snd (snd (snd p))))) (\p. size (snd p))) <*mlex*> case_sum (\x. Suc 0) (\x. 0) <*mlex*> case_sum (\x. 0) (case_sum (\x. Suc 0) (\x. 0)) <*mlex*> {}" signature WORD_LIB = sig val dest_binT: typ -> int val dest_wordT: typ -> int val is_wordT: typ -> bool val mk_wordT: int -> typ end structure Word_Lib: WORD_LIB structure SMT_Word: sig end ### theory "HOL-Word.Word" ### 5.798s elapsed time, 11.524s cpu time, 1.128s GC time Loading theory "Native_Word.Word_Misc" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32") class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Found termination order: "(\p. size (snd p)) <*mlex*> {}" locale quickcheck_narrowing_samples fixes a_of_integer :: "integer \ 'a \ 'a" and zero :: "'a" and tr :: "typerep" ### theory "Native_Word.Word_Misc" ### 1.035s elapsed time, 2.036s cpu time, 0.408s GC time Loading theory "Native_Word.Uint" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "HOL-ODE-Numerics.GenCF_No_Comp" via "Collections.Impl_Uv_Set") class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" consts rbt_map_entry :: "'a \ ('b \ 'b) \ ('a, 'b) rbt \ ('a, 'b) rbt" 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. 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 consts map :: "('a \ 'b \ 'c) \ ('a, 'b) rbt \ ('a, 'c) rbt" 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 class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" instantiation uint :: equal equal_uint == equal_class.equal :: uint \ uint \ bool instantiation uint :: size size_uint == size :: uint \ nat Found termination order: "(\p. size (fst (snd (snd p)))) <*mlex*> {}" ### Code generator: dropping subsumed code equation ### (!!) ?x \ (!!) (Rep_uint ?x) ### Code generator: dropping subsumed code equation ### lsb ?x \ lsb (Rep_uint ?x) ### Ambiguous input (line 720 of "~~/afp/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>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"))))) ### ("\<^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"))))) ### 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 724 of "~~/afp/thys/Native_Word/Uint.thy") produces 2 parse trees: ### ("\<^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"))))) ### ("\<^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"))))) ### 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 731 of "~~/afp/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>Uint.sshiftr_uint" ### ("_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>Word.sshiftr" ### ("_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 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 class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "Native_Word.Uint" ### 2.027s elapsed time, 3.992s cpu time, 0.720s GC time Loading theory "Native_Word.Uint32" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode") ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Numeral_Type.bit0" found. 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 instantiation uint32 :: linorder less_eq_uint32 == less_eq :: uint32 \ uint32 \ bool less_uint32 == less :: uint32 \ uint32 \ bool 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 uint32 :: equal equal_uint32 == equal_class.equal :: uint32 \ uint32 \ bool instantiation uint32 :: size size_uint32 == size :: uint32 \ nat ### Code generator: dropping subsumed code equation ### (!!) ?x \ (!!) (Rep_uint32 ?x) ### Code generator: dropping subsumed code equation ### lsb ?x \ lsb (Rep_uint32 ?x) ### Ambiguous input (line 567 of "~~/afp/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>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"))))) ### ("\<^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"))))) ### 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 571 of "~~/afp/thys/Native_Word/Uint32.thy") produces 2 parse trees: ### ("\<^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"))))) ### ("\<^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"))))) ### 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 577 of "~~/afp/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>Uint32.sshiftr_uint32" ### ("_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>Word.sshiftr" ### ("_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 ### theory "Native_Word.Uint32" ### 1.757s elapsed time, 3.524s cpu time, 0.000s GC time Loading theory "Collections.HashCode" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator") class hashable = type + fixes hashcode :: "'a \ uint32" and def_hashmap_size :: "'a itself \ nat" assumes "def_hashmap_size": "1 < def_hashmap_size TYPE('a)" instantiation unit :: hashable hashcode_unit == hashcode :: unit \ uint32 def_hashmap_size_unit == def_hashmap_size :: unit itself \ nat instantiation bool :: hashable hashcode_bool == hashcode :: bool \ uint32 def_hashmap_size_bool == def_hashmap_size :: bool itself \ nat instantiation int :: hashable hashcode_int == hashcode :: int \ uint32 def_hashmap_size_int == def_hashmap_size :: int itself \ nat instantiation integer :: hashable hashcode_integer == hashcode :: integer \ uint32 def_hashmap_size_integer == def_hashmap_size :: integer itself \ nat instantiation nat :: hashable hashcode_nat == hashcode :: nat \ uint32 def_hashmap_size_nat == def_hashmap_size :: nat itself \ nat instantiation char :: hashable hashcode_char == hashcode :: char \ uint32 def_hashmap_size_char == def_hashmap_size :: char itself \ nat instantiation prod :: (hashable, hashable) hashable hashcode_prod == hashcode :: 'a \ 'b \ uint32 def_hashmap_size_prod == def_hashmap_size :: ('a \ 'b) itself \ nat instantiation sum :: (hashable, hashable) hashable hashcode_sum == hashcode :: 'a + 'b \ uint32 def_hashmap_size_sum == def_hashmap_size :: ('a + 'b) itself \ nat instantiation list :: (hashable) hashable hashcode_list == hashcode :: 'a list \ uint32 def_hashmap_size_list == def_hashmap_size :: 'a list itself \ nat instantiation option :: (hashable) hashable hashcode_option == hashcode :: 'a option \ uint32 def_hashmap_size_option == def_hashmap_size :: 'a option itself \ nat instantiation String.literal :: hashable hashcode_literal == hashcode :: String.literal \ uint32 def_hashmap_size_literal == def_hashmap_size :: String.literal itself \ nat ### theory "Collections.HashCode" ### 0.648s elapsed time, 1.260s cpu time, 0.304s GC time Loading theory "Deriving.Hash_Generator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive" via "Deriving.Hash_Instances") Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" signature HASHCODE_GENERATOR = sig val ensure_info: hash_type -> string -> local_theory -> local_theory val generate_hash: hash_type -> string -> local_theory -> local_theory val generate_hashs_from_bnf_fp: string -> local_theory -> ((term * thm list) list * (term * thm) list) * local_theory val get_info: Proof.context -> string -> info option datatype hash_type = BNF | HASHCODE val hashable_instance: string -> theory -> theory type info = {hash: term, hash_def: thm option, map: term, map_comp: thm option, phash: term, used_positions: bool list} val register_foreign_hash: typ -> term -> local_theory -> local_theory val register_foreign_partial_and_full_hash: string -> term -> term -> term -> thm option -> thm option -> bool list -> local_theory -> local_theory val register_hash_of: string -> local_theory -> local_theory end structure Hashcode_Generator: HASHCODE_GENERATOR ### theory "Deriving.Hash_Generator" ### 0.944s elapsed time, 1.892s cpu time, 0.000s GC time Loading theory "Deriving.Hash_Instances" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive") generating hash-function for type "Product_Type.prod" generating hash-function for type "Sum_Type.sum" generating hash-function for type "Option.option" generating hash-function for type "List.list" ### theory "Deriving.Hash_Instances" ### 0.168s elapsed time, 0.340s cpu time, 0.000s GC time Loading theory "Deriving.Countable_Generator" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "Deriving.Derive") Found termination order: "case_sum (\p. size (fst p)) (\p. size (fst p)) <*mlex*> {}" ### theory "Deriving.Countable_Generator" ### 0.228s elapsed time, 0.460s cpu time, 0.000s GC time Loading theory "Deriving.Derive" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program") Found termination order: "size <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Found termination order: "{}" ### theory "Deriving.Derive" ### 1.232s elapsed time, 2.412s cpu time, 0.396s GC time Loading theory "Affine_Arithmetic.Optimize_Integer" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print" via "Affine_Arithmetic.Optimize_Float") ### theory "Affine_Arithmetic.Optimize_Integer" ### 0.328s elapsed time, 0.656s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Optimize_Float" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print") class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" ### Code generator: dropping subsumed code equation ### bitlen ?x \ if 0 < ?x then bitlen (?x div 2) + 1 else 0 ### Code generator: dropping subsumed code equation ### Float ?m1.0 ?e1.0 + Float ?m2.0 ?e2.0 \ ### if ?m1.0 = 0 then Float ?m2.0 ?e2.0 ### else if ?m2.0 = 0 then Float ?m1.0 ?e1.0 ### else if ?e1.0 \ ?e2.0 ### then Float (?m1.0 + ?m2.0 * 2 ^ nat (?e2.0 - ?e1.0)) ?e1.0 ### else Float (?m2.0 + ?m1.0 * 2 ^ nat (?e1.0 - ?e2.0)) ?e2.0 ### Code generator: dropping subsumed code equation ### real_of_float (Float ?m ?e) \ ### if 0 \ ?e then real_of_int ?m * 2 ^ nat ?e ### else real_of_int ?m / 2 ^ nat (- ?e) ### Code generator: dropping subsumed code equation ### float_down ?p (Float ?m ?e) \ ### if ?p + ?e < 0 then Float (div_twopow ?m (nat (- (?p + ?e)))) (- ?p) ### else Float ?m ?e ### Code generator: dropping subsumed code equation ### lapprox_posrat ?prec ?x ?y \ ### let l = rat_precision ?prec (int ?x) (int ?y); ### x = if 0 \ l then ?x * 2 ^ nat l div ?y ### else ?x div 2 ^ nat (- l) div ?y ### in normfloat (Float (int x) (- l)) ### Code generator: dropping subsumed code equation ### rapprox_posrat ?prec ?x ?y \ ### let l = rat_precision ?prec (int ?x) (int ?y); ### (r, s) = ### if 0 \ l then (int ?x * 2 ^ nat l, int ?y) ### else (int ?x, int ?y * 2 ^ nat (- l)); ### d = r div s; m = r mod s ### in normfloat (Float (d + (if m = 0 \ ?y = 0 then 0 else 1)) (- l)) ### Code generator: dropping subsumed code equation ### float_round_down ?prec (Float ?m ?e) \ ### let d = bitlen \?m\ - int ?prec - 1 ### in if 0 < d then Float (div_twopow ?m (nat d)) (?e + d) else Float ?m ?e ### Code generator: dropping subsumed code equation ### int_floor_fl (Float ?m ?e) \ ### if 0 \ ?e then ?m * 2 ^ nat ?e else ?m div 2 ^ nat (- ?e) ### Code generator: dropping subsumed code equation ### floor_fl (Float ?m ?e) \ ### if 0 \ ?e then Float ?m ?e else Float (?m div 2 ^ nat (- ?e)) 0 ### theory "Affine_Arithmetic.Optimize_Float" ### 0.374s elapsed time, 0.748s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Float_Real" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation") ### Code generator: dropping subsumed code equation ### 0 \ Ratreal 0 ### Code generator: dropping subsumed code equation ### 1 \ Ratreal 1 ### Constructor as head in equation, in theorem: ### real_of_float (Float ?m ?e) \ ### if 0 \ ?e then real_of_int ?m * 2 ^ nat ?e ### else real_of_int ?m / real_of_int (power_int 2 (- ?e)) ### theory "Affine_Arithmetic.Float_Real" ### 0.159s elapsed time, 0.320s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Counterclockwise" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Intersection" via "Affine_Arithmetic.Polygon" via "Affine_Arithmetic.Counterclockwise_2D_Strict" via "Affine_Arithmetic.Counterclockwise_Vector") locale linorder_list0 fixes le :: "'a \ 'a \ bool" Proofs for inductive predicate(s) "sortedP" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale linorder_list fixes le :: "'a \ 'a \ bool" and S :: "'a set" assumes "linorder_list le S" locale ccw_system0 fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" locale ccw_system12 fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_system12 ccw S" locale ccw_system123 fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_system123 ccw S" locale ccw_system4 fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_system4 ccw S" locale ccw_system1235' fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_system1235' ccw S" locale ccw_system1235 fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_system1235 ccw S" locale ccw_system fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_system ccw S" ### theory "Affine_Arithmetic.Counterclockwise" ### 0.805s elapsed time, 1.616s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Counterclockwise_Vector" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Intersection" via "Affine_Arithmetic.Polygon" via "Affine_Arithmetic.Counterclockwise_2D_Strict") locale ccw_vector_space fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" assumes "ccw_vector_space ccw S" locale ccw_convex fixes ccw :: "'a \ 'a \ 'a \ bool" and S :: "'a set" and oriented :: "'a \ 'a \ bool" assumes "ccw_convex ccw S oriented" ### theory "Affine_Arithmetic.Counterclockwise_Vector" ### 0.249s elapsed time, 0.500s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Counterclockwise_2D_Strict" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Intersection" via "Affine_Arithmetic.Polygon") Found termination order: "{}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### Ambiguous input (line 1812 of "~~/src/HOL/Library/RBT_Impl.thy") produces 2 parse trees: ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" sorted) ### ("_applC" ("_position" map) ### ("_cargs" ("_position" fst) ("_position" xs))))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" sorted) ### ("_applC" ("_position" map) ### ("_cargs" ("_position" fst) ("_position" ys))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" map_of) ### ("_cargs" ### ("_applC" ("_position" sunion_with) ### ("_cargs" ("_position" f) ### ("_cargs" ("_position" xs) ("_position" ys)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" map_of) ### ("_cargs" ("_position" xs) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" map_of) ### ("_cargs" ("_position" ys) ("_position" k)))) ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" map_of) ### ("_cargs" ("_position" ys) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Some) ("_position" v))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v) ### ("_position" w)))))))))))))) ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" sorted) ### ("_applC" ("_position" map) ### ("_cargs" ("_position" fst) ("_position" xs))))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" sorted) ### ("_applC" ("_position" map) ### ("_cargs" ("_position" fst) ("_position" ys))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" map_of) ### ("_cargs" ### ("_applC" ("_position" sunion_with) ### ("_cargs" ("_position" f) ### ("_cargs" ("_position" xs) ("_position" ys)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" map_of) ### ("_cargs" ("_position" xs) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" map_of) ### ("_cargs" ("_position" ys) ("_position" k)))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" map_of) ### ("_cargs" ("_position" ys) ("_position" k))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Some) ("_position" v))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v) ("_position" w)))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Affine_Arithmetic.Counterclockwise_2D_Strict" ### 1.142s elapsed time, 2.252s cpu time, 0.492s GC time Loading theory "Affine_Arithmetic.Counterclockwise_2D_Arbitrary" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Intersection") class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" ### theory "Affine_Arithmetic.Counterclockwise_2D_Arbitrary" ### 0.649s elapsed time, 1.304s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Polygon" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Intersection") class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### Ambiguous input (line 1926 of "~~/src/HOL/Library/RBT_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_applC" ("_position" rbt_insert_with_key) ("_position" f)) ### ("_cargs" ("_position" t1) ("_position" t2)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k)))) ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Some) ("_position" v))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" w) ("_position" v))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_applC" ("_position" rbt_insert_with_key) ("_position" f)) ### ("_cargs" ("_position" t1) ("_position" t2)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k)))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Some) ("_position" v))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" w) ("_position" v))))))))))) ### 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 1947 of "~~/src/HOL/Library/RBT_Impl.thy") produces 2 parse trees: ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t1))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t2))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ### ("_applC" ("_position" rbt_union_with_key) ### ("_cargs" ("_position" f) ### ("_cargs" ("_position" t1) ("_position" t2)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k)))) ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Some) ("_position" v))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v) ### ("_position" w)))))))))))))) ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t1))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t2))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ### ("_applC" ("_position" rbt_union_with_key) ### ("_cargs" ("_position" f) ### ("_cargs" ("_position" t1) ("_position" t2)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k)))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Some) ("_position" v))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v) ("_position" w)))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Found termination order: "{}" ### Ambiguous input (line 1978 of "~~/src/HOL/Library/RBT_Impl.thy") produces 2 parse trees: ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t1))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t2))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ### ("_applC" ("_position" rbt_inter_with_key) ### ("_cargs" ("_position" f) ### ("_cargs" ("_position" t1) ("_position" t2)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v) ### ("_position" w)))))))))))))) ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t1))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" rbt_sorted) ("_position" t2))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ### ("_applC" ("_position" rbt_inter_with_key) ### ("_cargs" ("_position" f) ### ("_cargs" ("_position" t1) ("_position" t2)))) ### ("_position" k))) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" v)) ### ("_case_syntax" ### ("_applC" ("_position" rbt_lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case1" ("_position" None) ("_position" None)))) ### ("_case1" ("_applC" ("_position" Some) ("_position" w)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v) ("_position" w)))))))))))) ### 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 ### ord.sunion_with ?less ?f ((?k, ?v) # ?as) ((?k', ?v') # ?bs) \ ### if ?less ?k' ?k ### then (?k', ?v') # ord.sunion_with ?less ?f ((?k, ?v) # ?as) ?bs ### else if ?less ?k ?k' ### then (?k, ?v) # ord.sunion_with ?less ?f ?as ((?k', ?v') # ?bs) ### else (?k, ?f ?k ?v ?v') # ord.sunion_with ?less ?f ?as ?bs ### Code generator: dropping subsumed code equation ### ord.sunion_with ?less ?f [] ?bs \ ?bs ### Code generator: dropping subsumed code equation ### ord.sunion_with ?less ?f ?as [] \ ?as ### Code generator: dropping subsumed code equation ### ord.sinter_with ?less ?f ((?k, ?v) # ?as) ((?k', ?v') # ?bs) \ ### if ?less ?k' ?k then ord.sinter_with ?less ?f ((?k, ?v) # ?as) ?bs ### else if ?less ?k ?k' then ord.sinter_with ?less ?f ?as ((?k', ?v') # ?bs) ### else (?k, ?f ?k ?v ?v') # ord.sinter_with ?less ?f ?as ?bs ### Code generator: dropping subsumed code equation ### ord.sinter_with ?less ?f [] ?uu \ [] ### Code generator: dropping subsumed code equation ### ord.sinter_with ?less ?f ?uv [] \ [] consts polychain_of :: "'a \ 'a list \ ('a \ 'a) list" ### Code generator: dropping subsumed code equation ### keys (Branch ?c ?l ?k ?v ?r) \ keys ?l @ ?k # keys ?r ### Code generator: dropping subsumed code equation ### keys Empty \ [] ### theory "HOL-Library.RBT_Impl" ### 37.766s elapsed time, 63.152s cpu time, 5.556s GC time Loading theory "HOL-Library.RBT" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program" via "HOL-Library.RBT_Mapping") consts dirvec :: "'a \ 'a \ 'a" ### theory "Affine_Arithmetic.Polygon" ### 0.873s elapsed time, 1.684s cpu time, 0.528s GC time Loading theory "Affine_Arithmetic.Affine_Form" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation") ### theory "HOL-Library.RBT" ### 0.916s elapsed time, 1.772s cpu time, 0.528s GC time Loading theory "HOL-Library.RBT_Mapping" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program") ### theory "HOL-Library.RBT_Mapping" ### 0.272s elapsed time, 0.548s cpu time, 0.000s GC time Loading theory "Affine_Arithmetic.Floatarith_Expression" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation" via "Affine_Arithmetic.Straight_Line_Program") instantiation pdevs :: (equal) equal equal_pdevs == equal_class.equal :: 'a pdevs \ 'a pdevs \ bool consts interpret_floatariths :: "floatarith list \ real list \ real list" instantiation floatarith :: {inverse,minus,one,plus,times,uminus,zero} zero_floatarith == zero_class.zero :: floatarith uminus_floatarith == uminus :: floatarith \ floatarith times_floatarith == times :: floatarith \ floatarith \ floatarith plus_floatarith == plus :: floatarith \ floatarith \ floatarith one_floatarith == one_class.one :: floatarith minus_floatarith == minus :: floatarith \ floatarith \ floatarith inverse_floatarith == inverse :: floatarith \ floatarith divide_floatarith == divide :: floatarith \ floatarith \ floatarith consts Sum\<^sub>e :: "('a \ 'b) \ 'a list \ 'b" Found termination order: "{}" Found termination order: "size <*mlex*> {}" ### theory "Affine_Arithmetic.Affine_Form" ### 4.580s elapsed time, 9.120s cpu time, 0.676s GC time Loading theory "Affine_Arithmetic.Intersection" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code") consts max_Var_floatarith :: "floatarith \ nat" consts max_Var_floatariths :: "floatarith list \ nat" consts max_Var_form :: "form \ nat" consts fresh_floatarith :: "floatarith \ nat \ bool" consts fresh_floatariths :: "floatarith list \ nat \ bool" Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" ### ML warning (line 980 of "~~/afp/thys/Affine_Arithmetic/Floatarith_Expression.thy"): ### Pattern is not exhaustive. ### ML warning (line 982 of "~~/afp/thys/Affine_Arithmetic/Floatarith_Expression.thy"): ### Pattern is not exhaustive. ### ML warning (line 1016 of "~~/afp/thys/Affine_Arithmetic/Floatarith_Expression.thy"): ### Pattern is not exhaustive. ### ML warning (line 1034 of "~~/afp/thys/Affine_Arithmetic/Floatarith_Expression.thy"): ### Pattern is not exhaustive. val mk_congeq = fn: Proof.context -> term list -> thm -> string list * thm val mk_congs = fn: Proof.context -> thm list -> (string list * thm) list * (typ * ('a list * 'b list)) list val interpret_floatariths_congs = fn: Proof.context -> thm list val preproc_form_conv = fn: Proof.context -> conv val reify_floatariths_tac = fn: Proof.context -> int -> tactic val interpret_floatariths_step_tac = fn: Proof.context -> int -> tactic Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "size <*mlex*> {}" Found termination order: "(\p. length (fst (snd p))) <*mlex*> {}" consts freshs_floatarith :: "floatarith \ nat list \ bool" Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" consts isnFDERIV :: "nat \ floatarith list \ nat list \ nat list \ real list \ nat \ bool" Found termination order: "length <*mlex*> {}" consts isnFDERIV_approx :: "nat \ nat \ floatarith list \ nat list \ nat list \ (float \ float) option list \ nat \ bool" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "{}" ### theory "Affine_Arithmetic.Floatarith_Expression" ### 9.808s elapsed time, 19.440s cpu time, 1.864s GC time Loading theory "Affine_Arithmetic.Straight_Line_Program" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code" via "Affine_Arithmetic.Affine_Approximation") Found termination order: "{}" consts bound_intersect_2d :: "nat \ ((real \ real) \ real \ real) list \ real \ (real \ real) option" ### theory "Affine_Arithmetic.Intersection" ### 6.469s elapsed time, 12.812s cpu time, 1.188s GC time Loading theory "HOL-ODE-Numerics.One_Step_Method" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Runge_Kutta") locale grid fixes t :: "nat \ real" assumes "grid t" Found termination order: "(\p. size (snd (snd (snd p)))) <*mlex*> {}" locale consistent_one_step fixes t0 :: "real" and t1 :: "real" and x :: "real \ 'a" and incr :: "real \ real \ 'a \ 'a" and p :: "nat" and B :: "real" and r :: "real" and L :: "real" assumes "consistent_one_step t0 t1 x incr p B r L" locale max_step fixes t :: "nat \ real" and t1 :: "real" and p :: "nat" and L :: "real" and B :: "real" and r :: "real" assumes "max_step t t1 p L B r" locale convergent_one_step fixes t0 :: "real" and t1 :: "real" and x :: "real \ 'a" and incr :: "real \ real \ 'a \ 'a" and p :: "nat" and B :: "real" and r :: "real" and L :: "real" and t :: "nat \ real" assumes "convergent_one_step t0 t1 x incr p B r L t" locale disturbed_one_step fixes t :: "nat \ real" and t1 :: "real" and s :: "real \ real \ 'a \ 'a" and s0 :: "'a" and x :: "real \ 'a" and incr :: "real \ real \ 'a \ 'a" and p :: "nat" and B :: "real" and L :: "real" assumes "disturbed_one_step t t1 s s0 x incr p B L" locale stable_one_step fixes t1 :: "real" and x :: "real \ 'a" and incr :: "real \ real \ 'a \ 'a" and p :: "nat" and B :: "real" and r :: "real" and L :: "real" and t :: "nat \ real" and s :: "real \ real \ 'a \ 'a" and s0 :: "'a" assumes "stable_one_step t1 x incr p B r L t s s0" locale rounded_one_step fixes t :: "nat \ real" and t1 :: "real" and x :: "real \ 'a" and incr :: "real \ real \ 'a \ 'a" and p :: "nat" and B :: "real" and r :: "real" and L :: "real" and incr' :: "real \ real \ 'a \ 'a" and x0' :: "'a" assumes "rounded_one_step t t1 x incr p B r L incr' x0'" ### theory "HOL-ODE-Numerics.One_Step_Method" ### 1.109s elapsed time, 2.160s cpu time, 0.428s GC time Loading theory "HOL-ODE-Numerics.Runge_Kutta" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List") Found termination order: "(\p. size (snd (snd (snd (snd (snd (snd p))))))) <*mlex*> {}" deriving "compare_order" instance for type "Float.float" deriving "compare" instance for type "Float.float" consts rk_eval_dynamic :: "(nat \ nat \ real) \ (nat \ real) \ (real \ 'a \ 'a) \ real \ real \ 'a \ nat \ nat \ 'a" deriving "linorder" instance for type "Approximation.floatarith" generating comparator for type "Approximation.floatarith" locale derivative_on_prod fixes T :: "real set" and X :: "'a set" and f :: "real \ 'a \ 'a" and f' :: "real \ 'a \ real \ 'a \ 'a" assumes "derivative_on_prod T X f f'" consts interpret_slp :: "floatarith list \ real list \ real list" Found termination order: "(\p. size (fst p)) <*mlex*> {}" locale derivative_norm_bounded fixes T :: "real set" and X :: "'a set" and f :: "real \ 'a \ 'a" and f' :: "real \ 'a \ real \ 'a \ 'a" and B :: "real" and B' :: "real" assumes "derivative_norm_bounded T X f f' B B'" locale grid_from fixes t :: "nat \ real" and t0 :: "real" assumes "grid_from t t0" locale euler_consistent fixes T :: "real set" and f :: "real \ 'a \ 'a" and X :: "'a set" and X' :: "'a set" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" and solution :: "real \ 'a" and t0 :: "real" and x0 :: "'a" and r :: "real" and e :: "real" assumes "euler_consistent T f X X' B f' B' solution t0 x0 r e" locale max_step1 fixes t :: "nat \ real" and t1 :: "real" and L :: "real" and B :: "real" and r :: "real" assumes "max_step1 t t1 L B r" consts slp_of_fas' :: "floatarith list \ (floatarith, nat) mapping \ floatarith list \ (floatarith, nat) mapping \ floatarith list" locale euler_convergent fixes X' :: "'a set" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" and solution :: "real \ 'a" and t0 :: "real" and x0 :: "'a" and r :: "real" and e :: "real" and T :: "real set" and f :: "real \ 'a \ 'a" and X :: "'a set" and t :: "nat \ real" assumes "euler_convergent X' B f' B' solution t0 x0 r e T f X t" locale ivp_rectangle_bounded_derivative fixes t0 :: "real" and T :: "real set" and x0 :: "'a" and b :: "real" and f :: "real \ 'a \ 'a" and X :: "'a set" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" and r :: "real" and e :: "real" assumes "ivp_rectangle_bounded_derivative t0 T x0 b f B f' B' r e" defines "X \ cball x0 b" locale euler_on_rectangle fixes t0 :: "real" and T :: "real set" and x0 :: "'a" and f :: "real \ 'a \ 'a" and X :: "'a set" and t :: "nat \ real" and e :: "real" and b :: "real" and r :: "real" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" assumes "euler_on_rectangle t0 T x0 f t e b r B f' B'" defines "X \ cball x0 b" locale euler_on_rectangle fixes t0 :: "real" and T :: "real set" and x0 :: "'a" and f :: "real \ 'a \ 'a" and X :: "'a set" and t :: "nat \ real" and e :: "real" and b :: "real" and r :: "real" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" assumes "euler_on_rectangle t0 T x0 f t e b r B f' B'" defines "X \ cball x0 b" locale euler_rounded_on_rectangle fixes t0 :: "real" and T :: "real set" and x0 :: "'a" and f :: "real \ 'a \ 'a" and X :: "'a set" and t :: "nat \ real" and t0' :: "real" and e1' :: "real" and e2' :: "real" and x0' :: "'a" and b :: "real" and r :: "real" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" and g :: "real \ 'a \ 'a" and e :: "int" assumes "euler_rounded_on_rectangle t0 T x0 f t t0' e1' e2' x0' b r B f' B' g e" defines "X \ cball x0 b" locale euler_rounded_on_rectangle fixes t0 :: "real" and T :: "real set" and x0 :: "'a" and f :: "real \ 'a \ 'a" and X :: "'a set" and t :: "nat \ real" and t0' :: "real" and e1' :: "real" and e2' :: "real" and x0' :: "'a" and b :: "real" and r :: "real" and B :: "real" and f' :: "real \ 'a \ real \ 'a \ 'a" and B' :: "real" and g :: "real \ 'a \ 'a" and e :: "int" assumes "euler_rounded_on_rectangle t0 T x0 f t t0' e1' e2' x0' b r B f' B' g e" defines "X \ cball x0 b" ### theory "HOL-ODE-Numerics.Runge_Kutta" ### 4.748s elapsed time, 9.412s cpu time, 0.688s GC time Loading theory "Refine_Monadic.Refine_Chapter" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "HOL-ODE-Numerics.Autoref_Misc" via "HOL-ODE-Numerics.Refine_Dflt_No_Comp" via "Refine_Monadic.Refine_Monadic") ### theory "Refine_Monadic.Refine_Chapter" ### 0.022s elapsed time, 0.044s cpu time, 0.000s GC time Loading theory "Show.Show" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print" via "Show.Show_Instances") class show = type + fixes shows_prec :: "nat \ 'a \ char list \ char list" and shows_list :: "'a list \ char list \ char list" assumes "shows_prec_append": "\p x r s. shows_prec p x (r @ s) = shows_prec p x r @ s" and "shows_list_append": "\xs r s. shows_list xs (r @ s) = shows_list xs r @ s" Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" instantiation char :: show shows_prec_char == shows_prec :: nat \ char \ char list \ char list shows_list_char == shows_list :: char list \ char list \ char list signature SHOW_GENERATOR = sig val generate_showsp: string -> local_theory -> local_theory val register_foreign_partial_and_full_showsp: string -> int -> term -> term -> thm option -> term -> thm option -> bool list -> thm -> local_theory -> local_theory val register_foreign_showsp: typ -> term -> thm -> local_theory -> local_theory val show_instance: string -> theory -> theory end structure Show_Generator: SHOW_GENERATOR instantiation list :: (show) show shows_prec_list == shows_prec :: nat \ 'a list \ char list \ char list shows_list_list == shows_list :: 'a list list \ char list \ char list ### theory "Show.Show" ### 1.334s elapsed time, 2.632s cpu time, 0.396s GC time Loading theory "Show.Show_Instances" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print") consts showsp_bool :: "nat \ bool \ char list \ char list" consts pshowsp_prod :: "nat \ (char list \ char list) \ (char list \ char list) \ char list \ char list" Found termination order: "{}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" deriving "show" instance for type "Option.option" generating show-function for type "Option.option" ### theory "Affine_Arithmetic.Straight_Line_Program" ### 9.038s elapsed time, 17.908s cpu time, 1.512s GC time Loading theory "Affine_Arithmetic.Affine_Approximation" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Affine_Code") deriving "show" instance for type "Sum_Type.sum" generating show-function for type "Sum_Type.sum" deriving "show" instance for type "Product_Type.prod" deriving "show" instance for type "Product_Type.unit" deriving "show" instance for type "HOL.bool" deriving "show" instance for type "Nat.nat" deriving "show" instance for type "Int.int" deriving "show" instance for type "Rat.rat" ### theory "Show.Show_Instances" ### 1.933s elapsed time, 3.812s cpu time, 0.356s GC time val mk_2elem_list = fn: term -> term -> term val mk_compr = fn: term -> term -> term val test1 = "[1, 2]": cterm val test2 = "{x \ {1, 2, 3}. 2 < x}": cterm val test3 = Const ("Groups.plus_class.plus", "nat \ nat \ nat") $ Bound 0 $ Bound 0: term val dest_pair_singleton = fn: term -> term val dest_nat_pair_singleton = fn: term -> term * term val dest_pair_singleton_T = fn: term -> (term * typ) * (term * typ) val dest_pair_lambda = fn: term -> string * typ * string * typ * term * term val foo = fn: term -> term * term * int * term * term "True" :: "bool" (if ?x \ ?y then if ?x = ?y then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?y = ?x then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?y \ ?x then ?P else ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x \ ?y then if ?x < ?y then ?Q else ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?x \ ?y then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?y < ?x then ?R else ?P) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?x = ?y then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x < ?y then ?Q else if ?y = ?x then ?P else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?y < ?x then ?R else ?Q) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?x < ?y then ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?y \ ?x then ?R else ?Q) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) (if ?x = ?y then ?P else if ?x \ ?y then ?Q else ?R) = (case compare ?x ?y of Eq \ ?P | Lt \ ?Q | Gt \ ?R) Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" consts points_of_aform :: "'a \ 'a pdevs \ 'a list" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### ?x1 - ?y1 \ ?x1 + ?y1 ### Ignoring duplicate rewrite rule: ### - ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?x1 div ?y1 \ ?x1 * ?y1 ### Ignoring duplicate rewrite rule: ### inverse ?y \ ?y Found termination order: "(\p. size (fst (snd p))) <*mlex*> {}" consts approx_floatariths_aformerr :: "nat \ floatarith list \ ((real \ real pdevs) \ real) list \ ((real \ real pdevs) \ real) list option" consts approx_slp :: "nat \ floatarith list \ ((real \ real pdevs) \ real) list \ ((real \ real pdevs) \ real) list option" ### theory "Affine_Arithmetic.Affine_Approximation" ### 11.112s elapsed time, 22.036s cpu time, 1.332s GC time Loading theory "Affine_Arithmetic.Affine_Code" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic") consts degree_list :: "(nat \ 'a) list \ nat" Found termination order: "(\p. size_list size (snd (snd (snd (snd p))))) <*mlex*> (\p. size_list size (fst (snd (snd (snd p))))) <*mlex*> {}" consts update_list :: "nat \ 'a \ (nat \ 'a) list \ (nat \ 'a) list" ### theory "Affine_Arithmetic.Affine_Code" ### 3.575s elapsed time, 7.068s cpu time, 0.580s GC time Loading theory "Affine_Arithmetic.Print" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation") deriving "show" instance for type "Float.float" ### Ignoring duplicate rewrite rule: ### ?y1 AND ?x1 AND ?z1 \ ?x1 AND ?y1 AND ?z1 consts showsp_float10 :: "nat \ float10 \ char list \ char list" deriving "show" instance for type "Print.float10" deriving "show" instance for type "Real.real" Found termination order: "{}" ### Metis: Unused theorems: "More_Bits_Int.int_shiftl_numeral_2" ### Ignoring duplicate rewrite rule: ### ?x1 BIT ?b1 >> Suc ?n1 \ ?x1 >> ?n1 ### theory "Affine_Arithmetic.Print" ### 3.387s elapsed time, 6.752s cpu time, 0.232s GC time Loading theory "Affine_Arithmetic.Ex_Affine_Approximation" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic") ### Metis: Unused theorems: "Nat.neq0_conv", "Num.numeral_class.numeral.numeral_One", "Num.semiring_char_0_class.zero_neq_numeral" Loading theory "Affine_Arithmetic.Ex_Ineqs" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic") Found termination order: "{}" Found termination order: "{}" ### theory "Affine_Arithmetic.Ex_Affine_Approximation" ### 1.115s elapsed time, 2.180s cpu time, 0.244s GC time Loading theory "Affine_Arithmetic.Ex_Inter" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List" via "Affine_Arithmetic.Affine_Arithmetic") consts prove_pos :: "(nat \ nat \ char list) list \ nat \ nat \ (nat \ (real \ real pdevs) list \ (real \ real pdevs) option) \ (real \ real pdevs) list list \ bool" locale experiment5672466 ### theory "Affine_Arithmetic.Ex_Ineqs" ### 0.982s elapsed time, 1.972s cpu time, 0.000s GC time ### 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 ### Ignoring duplicate rewrite rule: ### 0 OR ?y \ ?y ### Ignoring duplicate rewrite rule: ### ?y OR 0 \ ?y Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Testing conjecture with Quickcheck-random... Quickcheck found a counterexample: x = 1 y = - 1 Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: x = 0 y = - 1 Evaluated terms: x AND y = 0 x OR y = - 1 Testing conjecture with Quickcheck-narrowing... [1 of 5] Compiling Data_Bits ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Data_Bits.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Data_Bits.o ) [2 of 5] Compiling Typerep ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Typerep.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Typerep.o ) [3 of 5] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Generated_Code.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Generated_Code.o ) [4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Narrowing_Engine.o ) [5 of 5] Compiling Main ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Main.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/Main.o ) Linking /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5688090/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. ### Rule already declared as introduction (intro) ### \?b = ?f ?x; ?x \ ?A\ \ ?b \ ?f ` ?A val ri1 = fn: unit -> (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * Isabelle5681650.Generated_Code.real))))))))) * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * Isabelle5681650.Generated_Code.real)))))))) ) Isabelle5681650.Generated_Code.pdevs val ri2 = fn: unit -> (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * Isabelle5681650.Generated_Code.real))))))))) * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * Isabelle5681650.Generated_Code.real)))))))) ) Isabelle5681650.Generated_Code.pdevs val ri3 = fn: unit -> (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * ...))))))))) * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * (Isabelle5681650.Generated_Code.real * ...)))))))) ) Isabelle5681650.Generated_Code.pdevs val iter = fn: (unit -> 'a) -> int -> 'a ### Metis: Unused theorems: "local.combine_rbt_greater", "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_2", "local.ineqs_3", "local.ineqs_4", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_3", "local.ineqs_4", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_greater_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.rbt_greater_simps_2" ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans" ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_2", "local.ineqs_3", "local.ineqs_4", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_3", "local.ineqs_4", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_greater_simps_2", "local.rbt_less_trans" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans" ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans" ### Ignoring duplicate rewrite rule: ### \?k1 \| ?l1; ?k1 \| ?r1\ ### \ ?k1 \| combine ?l1 ?r1 \ True ### Ignoring duplicate rewrite rule: ### \?l1 |\ ?k1; ?r1 |\ ?k1\ ### \ combine ?l1 ?r1 |\ ?k1 \ True ### Ignoring duplicate rewrite rule: ### \?l1 |\ ?k1; ?r1 |\ ?k1\ ### \ combine ?l1 ?r1 |\ ?k1 \ True ### Ignoring duplicate rewrite rule: ### \?k1 \| ?l1; ?k1 \| ?r1\ ### \ ?k1 \| combine ?l1 ?r1 \ True val it = ((Ratreal (Frct (Int_of_integer 3675172506975, Int_of_integer 35184372088832)), (Ratreal (Frct (Int_of_integer 6675295890371, Int_of_integer 70368744177664)), (Ratreal (Frct (Int_of_integer 425436828397, Int_of_integer 4398046511104)), (Ratreal ( Frct (Int_of_integer 1733042442549, Int_of_integer 17592186044416) ), (Ratreal ( Frct (Int_of_integer 935559424677, Int_of_integer 8796093022208) ), (Ratreal ( Frct (Int_of_integer 3189948467849, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 6111640025081, Int_of_integer 70368744177664) ), (Ratreal ( Frct (Int_of_integer 1765907648565, Int_of_integer 17592186044416) ), (Ratreal ( Frct (Int_of_integer 4287226986379, Int_of_integer 35184372088832) ), Ratreal ( Frct (Int_of_integer 1661599626391, Int_of_integer 17592186044416) )))))))))), Pdevs ( Abs_slist [(Nat 9, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), Ratreal ( Frct (Int_of_integer 14126463083680059, Int_of_integer 35184372088832) ))))))))))), (Nat 8, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 6359770429741721, Int_of_integer 17592186044416) ), Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)))))))))))), (Nat 7, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 5486648307914813, Int_of_integer 17592186044416) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)))))))))))), (Nat 6, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 28158362808887967, Int_of_integer 70368744177664) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)))))))))))), (Nat 5, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 5089781140020457, Int_of_integer 17592186044416) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), Ratreal (Frct (..., ...)))))))))))), (Nat 4, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 11285561618366089, Int_of_integer 35184372088832) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), Ratreal (Frct (..., ...)))))))))))), (Nat 3, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 2809559666041635, Int_of_integer 8796093022208) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., Ratreal ...)))))))))), (Nat 2, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 694047938901645, Int_of_integer 2199023255552) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., ...)))))))))), (Nat 1, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 20918708496451027, Int_of_integer 70368744177664) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., ...)))))))))), (Nat 0, (Ratreal ( Frct (Int_of_integer 13854085216035039, Int_of_integer 35184372088832) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))] )): (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * ?.Generated_Code.real))))))))) * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * ?.Generated_Code.real)))))))) ) Generated_Code.pdevs ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Metis: Unused theorems: "Rings.comm_ring_1_class.minus_dvd_iff" ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Metis: Unused theorems: "Word.word_sint.Rep_inverse'", "Word.wi_hom_neg" ### Ignoring duplicate rewrite rule: ### \0 \ ?k1; ?k1 < ?l1\ ### \ ?k1 div ?l1 \ 0 ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y val it = ((Ratreal (Frct (Int_of_integer 188218823585, Int_of_integer 4398046511104)), (Ratreal (Frct (Int_of_integer 996097353883, Int_of_integer 17592186044416)), (Ratreal (Frct (Int_of_integer 948365824497, Int_of_integer 17592186044416)), (Ratreal ( Frct (Int_of_integer 2201721443595, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 2443026516719, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 214459600837, Int_of_integer 4398046511104) ), (Ratreal ( Frct (Int_of_integer 29911901005, Int_of_integer 549755813888) ), (Ratreal ( Frct (Int_of_integer 501043273417, Int_of_integer 8796093022208) ), (Ratreal ( Frct (Int_of_integer 852027638289, Int_of_integer 17592186044416) ), Ratreal ( Frct (Int_of_integer 2019138393217, Int_of_integer 35184372088832) )))))))))), Pdevs ( Abs_slist [(Nat 9, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), Ratreal ( Frct (Int_of_integer 21435438858502871, Int_of_integer 35184372088832) ))))))))))), (Nat 8, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 12249497583084103, Int_of_integer 17592186044416) ), Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)))))))))))), (Nat 7, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 13213234849176667, Int_of_integer 17592186044416) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)))))))))))), (Nat 6, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 3019856669361313, Int_of_integer 4398046511104) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)))))))))))), (Nat 5, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 1647687426801773, Int_of_integer 2199023255552) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), Ratreal (Frct (..., ...)))))))))))), (Nat 4, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 22472969804975691, Int_of_integer 35184372088832) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), Ratreal (Frct (..., ...)))))))))))), (Nat 3, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 21829032009041843, Int_of_integer 35184372088832) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., Ratreal ...)))))))))), (Nat 2, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 5875149991903409, Int_of_integer 8796093022208) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., ...)))))))))), (Nat 1, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal ( Frct (Int_of_integer 11977661173756259, Int_of_integer 17592186044416) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., ...)))))))))), (Nat 0, (Ratreal ( Frct (Int_of_integer 6976155025277863, Int_of_integer 8796093022208) ), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))] )): (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * ?.Generated_Code.real))))))))) * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * ?.Generated_Code.real)))))))) ) Generated_Code.pdevs ### Metis: Unused theorems: "Nat.semiring_1_class.of_nat_mult" ### Ignoring duplicate rewrite rule: ### ?y < ?n1 \ ?y mod ?n1 \ ?y ### Metis: Unused theorems: "Word.word_less_def" ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### \0 \ ?y; ?y < ?l1\ ### \ ?y mod ?l1 \ ?y ### Ignoring duplicate rewrite rule: ### Numeral1 \ 1::?'a1 ### Ignoring duplicate rewrite rule: ### Numeral1 \ 1::?'a1 val it = ((Ratreal (Frct (Int_of_integer 1213522450997, Int_of_integer 35184372088832)), (Ratreal (Frct (Int_of_integer 2260641433515, Int_of_integer 70368744177664)), (Ratreal (Frct (Int_of_integer 206208774147, Int_of_integer 4398046511104)), (Ratreal ( Frct (Int_of_integer 1644732334125, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 3507881085247, Int_of_integer 70368744177664) ), (Ratreal ( Frct (Int_of_integer 3432621667203, Int_of_integer 70368744177664) ), (Ratreal ( Frct (Int_of_integer 952001048627, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 2448939438483, Int_of_integer 70368744177664) ), (Ratreal ( Frct (Int_of_integer 749046360259, Int_of_integer 17592186044416) ), (Ratreal ( Frct (Int_of_integer 1613442646069, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 3341316496455, Int_of_integer 70368744177664) ), (Ratreal ( Frct (Int_of_integer 1421309288341, Int_of_integer 35184372088832) ), (Ratreal ( Frct (Int_of_integer 3342602395377, Int_of_integer 70368744177664) ), (Ratreal ( Frct (Int_of_integer 417664562057, Int_of_integer 8796093022208) ), (Ratreal ( Frct (Int_of_integer 2969022505117, Int_of_integer 70368744177664) ), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., ...))))))))))))))))))), Pdevs ( Abs_slist [(Nat 19, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))))))))))), (Nat 18, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))))))))))))))), (Nat 17, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))))))))), (Nat 16, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))))))))))))), (Nat 15, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))))))), (Nat 14, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))))))))))), (Nat 13, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))))), (Nat 12, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))))))))), (Nat 11, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))))), (Nat 10, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))))))), (Nat 9, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))))), (Nat 8, (Ratreal (Frct (Int_of_integer 0, Int_of_integer 1)), (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))))), (Nat 7, (Ratreal (Frct (..., ...)), (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...))))))), (Nat 6, (Ratreal (Frct (..., ...)), (Ratreal ..., (..., (..., (...)))))), (Nat 5, (Ratreal ..., (..., (..., (...))))), (Nat 4, (..., (..., (...)))), (..., (..., (...))), ...] )): (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * ...)))))))))) * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * (?.Generated_Code.real * ...)))))))) ) Generated_Code.pdevs ### theory "Affine_Arithmetic.Ex_Inter" ### 52.676s elapsed time, 102.292s cpu time, 3.268s GC time Loading theory "Affine_Arithmetic.Affine_Arithmetic" (required by "HOL-ODE-Numerics.ODE_Numerics" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" via "HOL-ODE-Numerics.Refine_Rigorous_Numerics" via "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" via "HOL-ODE-Numerics.Refine_Vector_List") ### theory "Affine_Arithmetic.Affine_Arithmetic" ### 1.243s elapsed time, 2.428s cpu time, 0.088s GC time ### Ignoring duplicate rewrite rule: ### Numeral1 \ 1::?'a1 ### Ignoring duplicate rewrite rule: ### Numeral1 \ 1::?'a1 ### Ignoring duplicate rewrite rule: ### ?n1 \ Suc (length ?kvs1) \ ### entries (fst (rbtreeify_g ?n1 ?kvs1)) \ take (?n1 - 1) ?kvs1 The following sorts can be derived comparator: generate comparators for given types, options: (linorder) or () compare: register types in class compare, options: (linorder) or () compare_order: register types in class compare_order, options: (linorder) or () countable: register datatypes is class countable equality: generate an equality function, options are () and (eq) hash_code: generate a hash function, options are () and (hashcode) hashable: register types in class hashable linorder: register types in class linorder, options: (linorder) or () ### Ignoring duplicate rewrite rule: ### of_nat (?m1 ^ ?n1) \ of_nat ?m1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_nat (?m1 * ?n1) \ of_nat ?m1 * of_nat ?n1 ### Ignoring duplicate rewrite rule: ### of_nat (?m1 ^ ?n1) \ of_nat ?m1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_nat (?m1 * ?n1) \ of_nat ?m1 * of_nat ?n1 Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> (\p. size_list size (fst (snd p))) <*mlex*> {}" ### Metis: Unused theorems: "local.ccw_axioms_3", "local.ccw_axioms_4", "local.prems_3", "local.prems_4", "local.prems_5", "local.prems_6", "local.prems_7", "local.prems_8" Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> (\p. size_list size (fst (snd p))) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### vector [?y, ?y1, ?z1] $ 1 \ ?y ### Ignoring duplicate rewrite rule: ### vector [?x1, ?y, ?z1] $ 2 \ ?y ### Ignoring duplicate rewrite rule: ### vector [?x1, ?y1, ?y] $ 3 \ ?y ### Metis: Unused theorems: "local.ccw_axioms_1", "local.ccw_axioms_2", "local.prems_6", "local.prems_7", "local.prems_8" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Ignoring duplicate rewrite rule: ### coll 0 ?y1 (?r1 *\<^sub>R ?x1) \ ?r1 = 0 \ coll 0 ?y1 ?x1 ### Ignoring duplicate rewrite rule: ### f (0::'a) \ 0::'b ### Ignoring duplicate rewrite rule: ### f (0::'a) \ 0::'b ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Metis: Unused theorems: "List.take_map" ### Ignoring duplicate rewrite rule: ### fold_const_fa (Add ?fa1.1 ?fa2.1) \ ### let (ffa1, ffa2) = (fold_const_fa ?fa1.1, fold_const_fa ?fa2.1) ### in case (dest_Num_fa ffa1, dest_Num_fa ffa2) of ### (None, None) \ Add ffa1 ffa2 ### | (None, Some a) \ if a = 0 then ffa1 else Add ffa1 (Num a) ### | (Some a, None) \ if a = 0 then ffa2 else Add (Num a) ffa2 ### | (Some a, Some b) \ Num (a + b) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Minus ?a1) \ ### case fold_const_fa ?a1 of ### Add floatarith1 floatarith2 \ ### Minus (Add floatarith1 floatarith2) ### | Minus floatarith \ Minus (Minus floatarith) ### | Mult floatarith1 floatarith2 \ ### Minus (Mult floatarith1 floatarith2) ### | Inverse floatarith \ Minus (Inverse floatarith) ### | Cos floatarith \ Minus (Cos floatarith) ### | floatarith.Arctan floatarith \ ### Minus (Arctan\<^sub>e floatarith) ### | Abs floatarith \ Minus (Abs floatarith) ### | floatarith.Max floatarith1 floatarith2 \ ### Minus (Max\<^sub>e floatarith1 floatarith2) ### | floatarith.Min floatarith1 floatarith2 \ ### Minus (Min\<^sub>e floatarith1 floatarith2) ### | floatarith.Pi \ Minus Pi\<^sub>e ### | Sqrt floatarith \ Minus (Sqrt floatarith) ### | Exp floatarith \ Minus (Exp floatarith) ### | Powr floatarith1 floatarith2 \ ### Minus (Powr floatarith1 floatarith2) ### | floatarith.Ln floatarith \ Minus (Ln\<^sub>e floatarith) ### | floatarith ^\<^sub>e nat \ Minus (floatarith ^\<^sub>e nat) ### | Floor floatarith \ Minus (Floor floatarith) ### | Var nat \ Minus (Var nat) | Num x \ Num (- x) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Mult ?fa1.1 ?fa2.1) \ ### let (ffa1, ffa2) = (fold_const_fa ?fa1.1, fold_const_fa ?fa2.1) ### in case (dest_Num_fa ffa1, dest_Num_fa ffa2) of ### (None, None) \ Mult ffa1 ffa2 ### | (None, Some a) \ ### if a = 0 then Num 0 else if a = 1 then ffa1 else Mult ffa1 (Num a) ### | (Some a, None) \ ### if a = 0 then Num 0 else if a = 1 then ffa2 else Mult (Num a) ffa2 ### | (Some a, Some b) \ Num (a * b) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Inverse ?a1) \ Inverse (fold_const_fa ?a1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Abs ?a1) \ ### case fold_const_fa ?a1 of ### Add floatarith1 floatarith2 \ Abs (Add floatarith1 floatarith2) ### | Minus floatarith \ Abs (Minus floatarith) ### | Mult floatarith1 floatarith2 \ ### Abs (Mult floatarith1 floatarith2) ### | Inverse floatarith \ Abs (Inverse floatarith) ### | Cos floatarith \ Abs (Cos floatarith) ### | floatarith.Arctan floatarith \ Abs (Arctan\<^sub>e floatarith) ### | Abs floatarith \ Abs (Abs floatarith) ### | floatarith.Max floatarith1 floatarith2 \ ### Abs (Max\<^sub>e floatarith1 floatarith2) ### | floatarith.Min floatarith1 floatarith2 \ ### Abs (Min\<^sub>e floatarith1 floatarith2) ### | floatarith.Pi \ Abs Pi\<^sub>e ### | Sqrt floatarith \ Abs (Sqrt floatarith) ### | Exp floatarith \ Abs (Exp floatarith) ### | Powr floatarith1 floatarith2 \ ### Abs (Powr floatarith1 floatarith2) ### | floatarith.Ln floatarith \ Abs (Ln\<^sub>e floatarith) ### | floatarith ^\<^sub>e nat \ Abs (floatarith ^\<^sub>e nat) ### | Floor floatarith \ Abs (Floor floatarith) ### | Var nat \ Abs (Var nat) ### | Num x \ Num \x\ ### Ignoring duplicate rewrite rule: ### fold_const_fa (Max\<^sub>e ?a1 ?b1) \ ### case (fold_const_fa ?a1, fold_const_fa ?b1) of ### (Add floatarith1 floatarith2, y) \ ### Max\<^sub>e (Add floatarith1 floatarith2) y ### | (Minus floatarith, y) \ Max\<^sub>e (Minus floatarith) y ### | (Mult floatarith1 floatarith2, y) \ ### Max\<^sub>e (Mult floatarith1 floatarith2) y ### | (Inverse floatarith, y) \ Max\<^sub>e (Inverse floatarith) y ### | (Cos floatarith, y) \ Max\<^sub>e (Cos floatarith) y ### | (floatarith.Arctan floatarith, y) \ ### Max\<^sub>e (Arctan\<^sub>e floatarith) y ### | (Abs floatarith, y) \ Max\<^sub>e (Abs floatarith) y ### | (floatarith.Max floatarith1 floatarith2, y) \ ### Max\<^sub>e (Max\<^sub>e floatarith1 floatarith2) y ### | (floatarith.Min floatarith1 floatarith2, y) \ ### Max\<^sub>e (Min\<^sub>e floatarith1 floatarith2) y ### | (floatarith.Pi, y) \ Max\<^sub>e Pi\<^sub>e y ### | (Sqrt floatarith, y) \ Max\<^sub>e (Sqrt floatarith) y ### | (Exp floatarith, y) \ Max\<^sub>e (Exp floatarith) y ### | (Powr floatarith1 floatarith2, y) \ ### Max\<^sub>e (Powr floatarith1 floatarith2) y ### | (floatarith.Ln floatarith, y) \ ### Max\<^sub>e (Ln\<^sub>e floatarith) y ### | (floatarith ^\<^sub>e nat, y) \ ### Max\<^sub>e (floatarith ^\<^sub>e nat) y ### | (Floor floatarith, y) \ Max\<^sub>e (Floor floatarith) y ### | (Var nat, y) \ Max\<^sub>e (Var nat) y ### | (Num xa, Add floatarith1 floatarith2) \ ### Max\<^sub>e (Num xa) (Add floatarith1 floatarith2) ### | (Num xa, Minus floatarith) \ ### Max\<^sub>e (Num xa) (Minus floatarith) ### | (Num xa, Mult floatarith1 floatarith2) \ ### Max\<^sub>e (Num xa) (Mult floatarith1 floatarith2) ### | (Num xa, Inverse floatarith) \ ### Max\<^sub>e (Num xa) (Inverse floatarith) ### | (Num xa, Cos floatarith) \ ### Max\<^sub>e (Num xa) (Cos floatarith) ### | (Num xa, floatarith.Arctan floatarith) \ ### Max\<^sub>e (Num xa) (Arctan\<^sub>e floatarith) ### | (Num xa, Abs floatarith) \ ### Max\<^sub>e (Num xa) (Abs floatarith) ### | (Num xa, floatarith.Max floatarith1 floatarith2) \ ### Max\<^sub>e (Num xa) (Max\<^sub>e floatarith1 floatarith2) ### | (Num xa, floatarith.Min floatarith1 floatarith2) \ ### Max\<^sub>e (Num xa) (Min\<^sub>e floatarith1 floatarith2) ### | (Num xa, floatarith.Pi) \ Max\<^sub>e (Num xa) Pi\<^sub>e ### | (Num xa, Sqrt floatarith) \ ### Max\<^sub>e (Num xa) (Sqrt floatarith) ### | (Num xa, Exp floatarith) \ ### Max\<^sub>e (Num xa) (Exp floatarith) ### | (Num xa, Powr floatarith1 floatarith2) \ ### Max\<^sub>e (Num xa) (Powr floatarith1 floatarith2) ### | (Num xa, floatarith.Ln floatarith) \ ### Max\<^sub>e (Num xa) (Ln\<^sub>e floatarith) ### | (Num xa, floatarith ^\<^sub>e nat) \ ### Max\<^sub>e (Num xa) (floatarith ^\<^sub>e nat) ### | (Num xa, Floor floatarith) \ ### Max\<^sub>e (Num xa) (Floor floatarith) ### | (Num xa, Var nat) \ Max\<^sub>e (Num xa) (Var nat) ### | (Num xa, Num ya) \ Num (max xa ya) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Min\<^sub>e ?a1 ?b1) \ ### case (fold_const_fa ?a1, fold_const_fa ?b1) of ### (Add floatarith1 floatarith2, y) \ ### Min\<^sub>e (Add floatarith1 floatarith2) y ### | (Minus floatarith, y) \ Min\<^sub>e (Minus floatarith) y ### | (Mult floatarith1 floatarith2, y) \ ### Min\<^sub>e (Mult floatarith1 floatarith2) y ### | (Inverse floatarith, y) \ Min\<^sub>e (Inverse floatarith) y ### | (Cos floatarith, y) \ Min\<^sub>e (Cos floatarith) y ### | (floatarith.Arctan floatarith, y) \ ### Min\<^sub>e (Arctan\<^sub>e floatarith) y ### | (Abs floatarith, y) \ Min\<^sub>e (Abs floatarith) y ### | (floatarith.Max floatarith1 floatarith2, y) \ ### Min\<^sub>e (Max\<^sub>e floatarith1 floatarith2) y ### | (floatarith.Min floatarith1 floatarith2, y) \ ### Min\<^sub>e (Min\<^sub>e floatarith1 floatarith2) y ### | (floatarith.Pi, y) \ Min\<^sub>e Pi\<^sub>e y ### | (Sqrt floatarith, y) \ Min\<^sub>e (Sqrt floatarith) y ### | (Exp floatarith, y) \ Min\<^sub>e (Exp floatarith) y ### | (Powr floatarith1 floatarith2, y) \ ### Min\<^sub>e (Powr floatarith1 floatarith2) y ### | (floatarith.Ln floatarith, y) \ ### Min\<^sub>e (Ln\<^sub>e floatarith) y ### | (floatarith ^\<^sub>e nat, y) \ ### Min\<^sub>e (floatarith ^\<^sub>e nat) y ### | (Floor floatarith, y) \ Min\<^sub>e (Floor floatarith) y ### | (Var nat, y) \ Min\<^sub>e (Var nat) y ### | (Num xa, Add floatarith1 floatarith2) \ ### Min\<^sub>e (Num xa) (Add floatarith1 floatarith2) ### | (Num xa, Minus floatarith) \ ### Min\<^sub>e (Num xa) (Minus floatarith) ### | (Num xa, Mult floatarith1 floatarith2) \ ### Min\<^sub>e (Num xa) (Mult floatarith1 floatarith2) ### | (Num xa, Inverse floatarith) \ ### Min\<^sub>e (Num xa) (Inverse floatarith) ### | (Num xa, Cos floatarith) \ ### Min\<^sub>e (Num xa) (Cos floatarith) ### | (Num xa, floatarith.Arctan floatarith) \ ### Min\<^sub>e (Num xa) (Arctan\<^sub>e floatarith) ### | (Num xa, Abs floatarith) \ ### Min\<^sub>e (Num xa) (Abs floatarith) ### | (Num xa, floatarith.Max floatarith1 floatarith2) \ ### Min\<^sub>e (Num xa) (Max\<^sub>e floatarith1 floatarith2) ### | (Num xa, floatarith.Min floatarith1 floatarith2) \ ### Min\<^sub>e (Num xa) (Min\<^sub>e floatarith1 floatarith2) ### | (Num xa, floatarith.Pi) \ Min\<^sub>e (Num xa) Pi\<^sub>e ### | (Num xa, Sqrt floatarith) \ ### Min\<^sub>e (Num xa) (Sqrt floatarith) ### | (Num xa, Exp floatarith) \ ### Min\<^sub>e (Num xa) (Exp floatarith) ### | (Num xa, Powr floatarith1 floatarith2) \ ### Min\<^sub>e (Num xa) (Powr floatarith1 floatarith2) ### | (Num xa, floatarith.Ln floatarith) \ ### Min\<^sub>e (Num xa) (Ln\<^sub>e floatarith) ### | (Num xa, floatarith ^\<^sub>e nat) \ ### Min\<^sub>e (Num xa) (floatarith ^\<^sub>e nat) ### | (Num xa, Floor floatarith) \ ### Min\<^sub>e (Num xa) (Floor floatarith) ### | (Num xa, Var nat) \ Min\<^sub>e (Num xa) (Var nat) ### | (Num xa, Num ya) \ Num (min xa ya) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Floor ?a1) \ ### case fold_const_fa ?a1 of ### Add floatarith1 floatarith2 \ ### Floor (Add floatarith1 floatarith2) ### | Minus floatarith \ Floor (Minus floatarith) ### | Mult floatarith1 floatarith2 \ ### Floor (Mult floatarith1 floatarith2) ### | Inverse floatarith \ Floor (Inverse floatarith) ### | Cos floatarith \ Floor (Cos floatarith) ### | floatarith.Arctan floatarith \ ### Floor (Arctan\<^sub>e floatarith) ### | Abs floatarith \ Floor (Abs floatarith) ### | floatarith.Max floatarith1 floatarith2 \ ### Floor (Max\<^sub>e floatarith1 floatarith2) ### | floatarith.Min floatarith1 floatarith2 \ ### Floor (Min\<^sub>e floatarith1 floatarith2) ### | floatarith.Pi \ Floor Pi\<^sub>e ### | Sqrt floatarith \ Floor (Sqrt floatarith) ### | Exp floatarith \ Floor (Exp floatarith) ### | Powr floatarith1 floatarith2 \ ### Floor (Powr floatarith1 floatarith2) ### | floatarith.Ln floatarith \ Floor (Ln\<^sub>e floatarith) ### | floatarith ^\<^sub>e nat \ Floor (floatarith ^\<^sub>e nat) ### | Floor floatarith \ Floor (Floor floatarith) ### | Var nat \ Floor (Var nat) ### | Num x \ Num (floor_fl x) ### Ignoring duplicate rewrite rule: ### fold_const_fa (?a1 ^\<^sub>e ?b1) \ ### case fold_const_fa ?a1 of ### Add floatarith1 floatarith2 \ ### Add floatarith1 floatarith2 ^\<^sub>e ?b1 ### | Minus floatarith \ Minus floatarith ^\<^sub>e ?b1 ### | Mult floatarith1 floatarith2 \ ### Mult floatarith1 floatarith2 ^\<^sub>e ?b1 ### | Inverse floatarith \ Inverse floatarith ^\<^sub>e ?b1 ### | Cos floatarith \ Cos floatarith ^\<^sub>e ?b1 ### | floatarith.Arctan floatarith \ ### Arctan\<^sub>e floatarith ^\<^sub>e ?b1 ### | Abs floatarith \ Abs floatarith ^\<^sub>e ?b1 ### | floatarith.Max floatarith1 floatarith2 \ ### Max\<^sub>e floatarith1 floatarith2 ^\<^sub>e ?b1 ### | floatarith.Min floatarith1 floatarith2 \ ### Min\<^sub>e floatarith1 floatarith2 ^\<^sub>e ?b1 ### | floatarith.Pi \ Pi\<^sub>e ^\<^sub>e ?b1 ### | Sqrt floatarith \ Sqrt floatarith ^\<^sub>e ?b1 ### | Exp floatarith \ Exp floatarith ^\<^sub>e ?b1 ### | Powr floatarith1 floatarith2 \ ### Powr floatarith1 floatarith2 ^\<^sub>e ?b1 ### | floatarith.Ln floatarith \ Ln\<^sub>e floatarith ^\<^sub>e ?b1 ### | floatarith ^\<^sub>e nat \ ### (floatarith ^\<^sub>e nat) ^\<^sub>e ?b1 ### | Floor floatarith \ Floor floatarith ^\<^sub>e ?b1 ### | Var nat \ Var nat ^\<^sub>e ?b1 ### | Num x \ Num (x ^ ?b1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Cos ?a1) \ Cos (fold_const_fa ?a1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Arctan\<^sub>e ?a1) \ ### Arctan\<^sub>e (fold_const_fa ?a1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Sqrt ?a1) \ Sqrt (fold_const_fa ?a1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Exp ?a1) \ Exp (fold_const_fa ?a1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Ln\<^sub>e ?a1) \ Ln\<^sub>e (fold_const_fa ?a1) ### Ignoring duplicate rewrite rule: ### fold_const_fa (Powr ?a1 ?b1) \ ### Powr (fold_const_fa ?a1) (fold_const_fa ?b1) ### Ignoring duplicate rewrite rule: ### fold_const_fa Pi\<^sub>e \ Pi\<^sub>e ### Ignoring duplicate rewrite rule: ### fold_const_fa (Var ?v1) \ Var ?v1 ### Ignoring duplicate rewrite rule: ### fold_const_fa (Num ?x1) \ Num ?x1 ### Metis: Falling back on "metis (full_types)"... ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### ?i1 < length ?fas1 \ ### FDERIV_floatariths ?fas1 ?xs1 ?ds1 ! ?i1 \ ### FDERIV_floatarith (?fas1 ! ?i1) ?xs1 ?ds1 ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Metis: Unused theorems: "Floatarith_Expression.dest_Num_fa.simps_1", "Option.option.simps_3" ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Ignoring duplicate safe introduction (intro!) ### \closed ?s; continuous_on UNIV ?f\ ### \ closed (?f -` ?s) ### Rule already declared as introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Rule already declared as introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ennreal (?f x)) \ ennreal ?x) ?F ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Rule already declared as introduction (intro) ### bounded ?S \ bounded (closure ?S) ### Rule already declared as introduction (intro) ### convex ?S \ convex (closure ?S) ### Ignoring duplicate rewrite rule: ### convex (convex hull ?s1) \ True ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \ (1::?'a1) + of_nat ?m1 ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Rule already declared as introduction (intro) ### \?b = ?f ?x; ?x \ ?A\ \ ?b \ ?f ` ?A ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### closed ((\x. ?f1 x + ?y1) ` ?S1) \ closed (?f1 ` ?S1) ### Ignoring duplicate rewrite rule: ### closed ((\x. ?y1 + ?f1 x) ` ?S1) \ closed (?f1 ` ?S1) ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Metis: Unused theorems: "local.interpret_Unop_2" ### Metis: Unused theorems: "local.interpret_Unop_2" ### Ignoring duplicate rewrite rule: ### ?n1 < length ?fas1 \ ### interpret_floatariths ?fas1 ?xs1 ! ?n1 \ ### interpret_floatarith (?fas1 ! ?n1) ?xs1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 after unfold_tac 1. (shows_pl :001 \ shows_string ''Some'' \ shows_space \ show\<^sub>'\<^sub>a 1 :000 \ shows_pr :001) (:002 @ :003) = (shows_pl :001 \ shows_string ''Some'' \ shows_space \ show\<^sub>'\<^sub>a 1 :000 \ shows_pr :001) :002 @ :003 after unfold_tac 1. shows_string ''None'' (:001 @ :002) = shows_string ''None'' :001 @ :002 after unfold_tac 1. (shows_pl :001 \ shows_string ''Inr'' \ shows_space \ show\<^sub>'\<^sub>b 1 :000 \ shows_pr :001) (:002 @ :003) = (shows_pl :001 \ shows_string ''Inr'' \ shows_space \ show\<^sub>'\<^sub>b 1 :000 \ shows_pr :001) :002 @ :003 after unfold_tac 1. (shows_pl :001 \ shows_string ''Inl'' \ shows_space \ show\<^sub>'\<^sub>a 1 :000 \ shows_pr :001) (:002 @ :003) = (shows_pl :001 \ shows_string ''Inl'' \ shows_space \ show\<^sub>'\<^sub>a 1 :000 \ shows_pr :001) :002 @ :003 ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) "float_plus_down" :: "nat \ float \ float \ float" ### Ignoring duplicate rewrite rule: ### length Basis_list \ DIM(?'a1) ### Ignoring duplicate rewrite rule: ### length Basis_list \ DIM(?'a1) ### Ignoring duplicate rewrite rule: ### length Basis_list \ DIM(?'a1) linarith_split_limit exceeded (current value is 9) ### Ignoring duplicate rewrite rule: ### pdevs_apply (trunc_pdevs ?p1 ?X1) ?n1 \ ### eucl_truncate_down ?p1 (pdevs_apply ?X1 ?n1) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### ?a1 + ?b1 + ?c1 \ ?a1 + (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 + ?b1 \ ?b1 + ?a1 ### Ignoring duplicate rewrite rule: ### ?b1 + (?a1 + ?c1) \ ?a1 + (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 * ?c1 \ ?a1 * (?b1 * ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 \ ?b1 * ?a1 ### Ignoring duplicate rewrite rule: ### ?b1 * (?a1 * ?c1) \ ?a1 * (?b1 * ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 - ?c1 \ ?a1 - (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 + (?b1 - ?c1) \ ?a1 + ?b1 - ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 = ?c1 \ ?a1 = ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 = ?c1 - ?b1 \ ?a1 + ?b1 = ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - (?b1 - ?c1) \ ?a1 + ?c1 - ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 + ?c1 \ ?a1 + ?c1 - ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 < ?c1 \ ?a1 < ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 < ?c1 - ?b1 \ ?a1 + ?b1 < ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 \ ?c1 \ ?a1 \ ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 \ ?c1 - ?b1 \ ?a1 + ?b1 \ ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 + ?b1 + ?c1 \ ?a1 + (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 + ?b1 \ ?b1 + ?a1 ### Ignoring duplicate rewrite rule: ### ?b1 + (?a1 + ?c1) \ ?a1 + (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 * ?c1 \ ?a1 * (?b1 * ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 \ ?b1 * ?a1 ### Ignoring duplicate rewrite rule: ### ?b1 * (?a1 * ?c1) \ ?a1 * (?b1 * ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 - ?c1 \ ?a1 - (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 + (?b1 - ?c1) \ ?a1 + ?b1 - ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 = ?c1 \ ?a1 = ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 = ?c1 - ?b1 \ ?a1 + ?b1 = ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - (?b1 - ?c1) \ ?a1 + ?c1 - ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 + ?c1 \ ?a1 + ?c1 - ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 < ?c1 \ ?a1 < ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 < ?c1 - ?b1 \ ?a1 + ?b1 < ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 \ ?c1 \ ?a1 \ ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 \ ?c1 - ?b1 \ ?a1 + ?b1 \ ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 + ?b1 + ?c1 \ ?a1 + (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 + ?b1 \ ?b1 + ?a1 ### Ignoring duplicate rewrite rule: ### ?b1 + (?a1 + ?c1) \ ?a1 + (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 * ?c1 \ ?a1 * (?b1 * ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 * ?b1 \ ?b1 * ?a1 ### Ignoring duplicate rewrite rule: ### ?b1 * (?a1 * ?c1) \ ?a1 * (?b1 * ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 - ?c1 \ ?a1 - (?b1 + ?c1) ### Ignoring duplicate rewrite rule: ### ?a1 + (?b1 - ?c1) \ ?a1 + ?b1 - ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 = ?c1 \ ?a1 = ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 = ?c1 - ?b1 \ ?a1 + ?b1 = ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - (?b1 - ?c1) \ ?a1 + ?c1 - ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 + ?c1 \ ?a1 + ?c1 - ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 < ?c1 \ ?a1 < ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 < ?c1 - ?b1 \ ?a1 + ?b1 < ?c1 ### Ignoring duplicate rewrite rule: ### ?a1 - ?b1 \ ?c1 \ ?a1 \ ?c1 + ?b1 ### Ignoring duplicate rewrite rule: ### ?a1 \ ?c1 - ?b1 \ ?a1 + ?b1 \ ?c1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 \ (1::?'a1) / ?a1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 \ (1::?'a1) / ?a1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 \ (1::?'a1) / ?a1 ### Metis: Unused theorems: "Affine_Approximation.degree_aform_err_add_aform'", "Affine_Approximation.degree_aform_ivl_err", "Groups.canonically_ordered_monoid_add_class.zero_le" ### Rule already declared as introduction (intro) ### degree ?x \ ?j \ pdevs_apply ?x ?j = (0::?'a) INFIMUM ?A Sup = SUPREMUM {f ` ?A |f. \Y\?A. f Y \ Y} Inf "[(FloatR 128 51, pdevs [(47, FloatR 0 0), (46, FloatR 2 41), (45, FloatR 2 40), (44, FloatR 2 39), (43, FloatR 2 38), (42, FloatR 2 37), (41, FloatR 2 36), (40, FloatR 2 35), (39, FloatR 2 34), (38, FloatR 2 33), (37, FloatR 2 32), (36, FloatR 2 31), (35, FloatR 2 30), (34, FloatR 2 29), (33, FloatR 2 28), (32, FloatR 2 27), (31, FloatR 2 26), (30, FloatR 2 25), (29, FloatR 2 24), (28, FloatR 2 23), (27, FloatR 2 22), (26, FloatR 2 21), (25, FloatR 2 20), (24, FloatR 2 19), (23, FloatR 2 18), (22, FloatR 2 17), (21, FloatR 2 16), (20, FloatR 2 15), (19, FloatR 2 14), (18, FloatR 2 13), (17, FloatR 2 12), (16, FloatR 2 11), (15, FloatR 2 10), (14, FloatR 2 9), (13, FloatR 2 8), (12, FloatR 2 7), (11, FloatR 2 6), (10, FloatR 2 5), (9, FloatR 2 4), (8, FloatR 2 3), (7, FloatR 2 2), (6, FloatR 1 1), (5, FloatR 1 0), (4, FloatR 192 42), (3, FloatR 191 42), (2, FloatR 5 (- 1)), (1, FloatR 255 42), (0, FloatR 1 (- 1))]), (FloatR 128 51, pdevs [(47, FloatR 0 0), (46, FloatR 0 0), (45, FloatR 0 0), (44, FloatR 0 0), (43, FloatR 0 0), (42, FloatR 0 0), (41, FloatR 0 0), (40, FloatR 0 0), (39, FloatR 0 0), (38, FloatR 0 0), (37, FloatR 0 0), (36, FloatR 0 0), (35, FloatR 0 0), (34, FloatR 0 0), (33, FloatR 0 0), (32, FloatR 0 0), (31, FloatR 0 0), (30, FloatR 0 0), (29, FloatR 0 0), (28, FloatR 0 0), (27, FloatR 0 0), (26, FloatR 0 0), (25, FloatR 0 0), (24, FloatR 0 0), (23, FloatR 0 0), (22, FloatR 0 0), (21, FloatR 0 0), (20, FloatR 0 0), (19, FloatR 0 0), (18, FloatR 0 0), (17, FloatR 0 0), (16, FloatR 0 0), (15, FloatR 0 0), (14, FloatR 0 0), (13, FloatR 0 0), (12, FloatR 0 0), (11, FloatR 0 0), (10, FloatR 0 0), (9, FloatR 0 0), (8, FloatR 0 0), (7, FloatR 0 0), (6, FloatR 0 0), (4, FloatR 192 42), (3, FloatR 192 42), (2, FloatR 0 0), (1, FloatR 128 43)]), (FloatR 128 51, pdevs [(48, FloatR 0 0), (47, FloatR 0 0), (46, FloatR 0 0), (45, FloatR 0 0), (44, FloatR 0 0), (43, FloatR 0 0), (42, FloatR 0 0), (41, FloatR 0 0), (40, FloatR 0 0), (39, FloatR 0 0), (38, FloatR 0 0), (37, FloatR 0 0), (36, FloatR 0 0), (35, FloatR 0 0), (34, FloatR 0 0), (33, FloatR 0 0), (32, FloatR 0 0), (31, FloatR 0 0), (30, FloatR 0 0), (29, FloatR 0 0), (28, FloatR 0 0), (27, FloatR 0 0), (26, FloatR 0 0), (25, FloatR 0 0), (24, FloatR 0 0), (23, FloatR 0 0), (22, FloatR 0 0), (21, FloatR 0 0), (20, FloatR 0 0), (19, FloatR 0 0), (18, FloatR 0 0), (17, FloatR 0 0), (16, FloatR 0 0), (15, FloatR 0 0), (14, FloatR 0 0), (13, FloatR 0 0), (12, FloatR 0 0), (11, FloatR 0 0), (10, FloatR 0 0), (9, FloatR 0 0), (8, FloatR 0 0), (7, FloatR 0 0), (6, FloatR 0 0), (4, FloatR 192 42), (3, FloatR 192 42), (2, FloatR 0 0), (1, FloatR 128 43)])]" :: "(real \ real pdevs) list" "((FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), pdevs [(211, FloatR 0 0, FloatR 0 0, FloatR 1214694609 (- 4)), (210, FloatR 0 0, FloatR 1214694609 (- 4), FloatR 0 0), (209, FloatR 1214694609 (- 4), FloatR 0 0, FloatR 0 0), (207, FloatR 0 (- 5), FloatR 0 (- 5), FloatR 0 (- 5)), (206, FloatR 0 0, FloatR 0 0, FloatR 0 0), (204, FloatR 0 (- 6), FloatR 0 (- 6), FloatR 0 (- 6)), (203, FloatR 0 0, FloatR 0 0, FloatR 0 0), (201, FloatR 0 (- 7), FloatR 0 (- 7), FloatR 0 (- 7)), (200, FloatR 0 0, FloatR 0 0, FloatR 0 0), (198, FloatR 0 (- 8), FloatR 0 (- 8), FloatR 0 (- 8)), (197, FloatR 0 0, FloatR 0 0, FloatR 0 0), (195, FloatR 0 (- 9), FloatR 0 (- 9), FloatR 0 (- 9)), (194, FloatR 0 0, FloatR 0 0, FloatR 0 0), (192, FloatR 0 (- 10), FloatR 0 (- 10), FloatR 0 (- 10)), (191, FloatR 0 0, FloatR 0 0, FloatR 0 0), (189, FloatR 0 (- 11), FloatR 0 (- 11), FloatR 0 (- 11)), (188, FloatR 0 0, FloatR 0 0, FloatR 0 0), (186, FloatR 0 (- 12), FloatR 0 (- 12), FloatR 0 (- 12)), (185, FloatR 0 0, FloatR 0 0, FloatR 0 0), (183, FloatR 0 (- 13), FloatR 0 (- 13), FloatR 0 (- 13)), (182, FloatR 0 0, FloatR 0 0, FloatR 0 0), (180, FloatR 0 (- 14), FloatR 0 (- 14), FloatR 0 (- 14)), (179, FloatR 0 0, FloatR 0 0, FloatR 0 0), (177, FloatR 0 (- 15), FloatR 0 (- 15), FloatR 0 (- 15)), (176, FloatR 0 0, FloatR 0 0, FloatR 0 0), (174, FloatR 0 (- 16), FloatR 0 (- 16), FloatR 0 (- 16)), (173, FloatR 0 0, FloatR 0 0, FloatR 0 0), (171, FloatR 0 (- 17), FloatR 0 (- 17), FloatR 0 (- 17)), (170, FloatR 0 0, FloatR 0 0, FloatR 0 0), (168, FloatR 0 (- 18), FloatR 0 (- 18), FloatR 0 (- 18)), (167, FloatR 0 0, FloatR 0 0, FloatR 0 0), (165, FloatR 0 (- 19), FloatR 0 (- 19), FloatR 0 (- 19)), (164, FloatR 0 0, FloatR 0 0, FloatR 0 0), (162, FloatR 0 (- 20), FloatR 0 (- 20), FloatR 0 (- 20)), (161, FloatR 0 0, FloatR 0 0, FloatR 0 0), (159, FloatR 0 (- 21), FloatR 0 (- 21), FloatR 0 (- 21)), (158, FloatR 0 0, FloatR 0 0, FloatR 0 0), (156, FloatR 0 (- 22), FloatR 0 (- 22), FloatR 0 (- 22)), (155, FloatR 0 0, FloatR 0 0, FloatR 0 0), (153, FloatR 0 (- 27), FloatR 0 (- 27), FloatR 0 (- 27)), (152, FloatR 0 0, FloatR 0 0, FloatR 0 0), (151, FloatR 0 (- 35), FloatR 0 (- 35), FloatR 0 (- 35)), (150, FloatR 0 (- 29), FloatR 0 (- 29), FloatR 0 (- 29)), (149, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (148, FloatR 0 (- 35), FloatR 0 (- 35), FloatR 0 (- 35)), (147, FloatR 0 (- 31), FloatR 0 (- 31), FloatR 0 (- 31)), (146, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (145, FloatR 0 (- 36), FloatR 0 (- 36), FloatR 0 (- 36)), (144, FloatR 0 (- 32), FloatR 0 (- 32), FloatR 0 (- 32)), (143, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (142, FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), (141, FloatR 0 (- 33), FloatR 0 (- 33), FloatR 0 (- 33)), (140, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (139, FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), (138, FloatR 0 (- 33), FloatR 0 (- 33), FloatR 0 (- 33)), (137, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (136, FloatR 0 (- 38), FloatR 0 (- 38), FloatR 0 (- 38)), (135, FloatR 0 (- 34), FloatR 0 (- 34), FloatR 0 (- 34)), (134, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (133, FloatR 0 (- 38), FloatR 0 (- 38), FloatR 0 (- 38)), (132, FloatR 0 (- 34), FloatR 0 (- 34), FloatR 0 (- 34)), (131, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (130, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (129, FloatR 0 (- 35), FloatR 0 (- 35), FloatR 0 (- 35)), (128, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (127, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (126, FloatR 0 (- 35), FloatR 0 (- 35), FloatR 0 (- 35)), (125, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (124, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (123, FloatR 0 (- 36), FloatR 0 (- 36), FloatR 0 (- 36)), (122, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (121, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (120, FloatR 0 (- 36), FloatR 0 (- 36), FloatR 0 (- 36)), (119, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (118, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (117, FloatR 0 (- 36), FloatR 0 (- 36), FloatR 0 (- 36)), (116, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (115, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (114, FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), (113, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (112, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (111, FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), (110, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (109, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (108, FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), (107, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (106, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (105, FloatR 0 (- 38), FloatR 0 (- 38), FloatR 0 (- 38)), (104, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (103, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (102, FloatR 0 (- 38), FloatR 0 (- 38), FloatR 0 (- 38)), (101, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (100, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (99, FloatR 0 (- 38), FloatR 0 (- 38), FloatR 0 (- 38)), (98, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (97, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (96, FloatR 0 (- 38), FloatR 0 (- 38), FloatR 0 (- 38)), (95, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (94, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (93, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (92, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (91, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (90, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (89, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (88, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (87, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (86, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (85, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (84, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (83, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (82, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (81, FloatR 0 (- 39), FloatR 0 (- 39), FloatR 0 (- 39)), (80, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (79, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (78, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (77, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (76, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (75, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (74, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (73, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (72, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (71, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (70, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (69, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40)), (68, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (67, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (66, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (65, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (64, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (63, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (62, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (61, FloatR 0 (- 45), FloatR 0 (- 45), FloatR 0 (- 45)), (60, FloatR 0 (- 41), FloatR 0 (- 41), FloatR 0 (- 41)), (59, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (58, FloatR 0 (- 45), FloatR 0 (- 45), FloatR 0 (- 45)), (57, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (56, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (55, FloatR 0 (- 45), FloatR 0 (- 45), FloatR 0 (- 45)), (54, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (53, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (52, FloatR 0 (- 45), FloatR 0 (- 45), FloatR 0 (- 45)), (51, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (50, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (49, FloatR 0 (- 45), FloatR 0 (- 45), FloatR 0 (- 45)), (48, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (47, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (46, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (45, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (44, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (43, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (42, FloatR 0 (- 45), FloatR 0 (- 45), FloatR 0 (- 45)), (41, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (40, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (39, FloatR 0 (- 47), FloatR 0 (- 47), FloatR 0 (- 47)), (38, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (37, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (36, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (35, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (34, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (33, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (32, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (31, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (30, FloatR 0 (- 44), FloatR 0 (- 44), FloatR 0 (- 44)), (29, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (28, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (27, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (26, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (25, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (24, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (23, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (22, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (21, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (20, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (19, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (18, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (17, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (16, FloatR 0 (- 46), FloatR 0 (- 46), FloatR 0 (- 46)), (15, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (14, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (13, FloatR 0 (- 47), FloatR 0 (- 47), FloatR 0 (- 47)), (12, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (11, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (10, FloatR 0 (- 47), FloatR 0 (- 47), FloatR 0 (- 47)), (9, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (8, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (7, FloatR 0 (- 47), FloatR 0 (- 47), FloatR 0 (- 47)), (6, FloatR 0 (- 42), FloatR 0 (- 42), FloatR 0 (- 42)), (5, FloatR 0 (- 43), FloatR 0 (- 43), FloatR 0 (- 43)), (4, FloatR 0 (- 67), FloatR 0 (- 67), FloatR 0 (- 67)), (3, FloatR 0 (- 62), FloatR 0 (- 62), FloatR 0 (- 62)), (2, FloatR 0 (- 63), FloatR 0 (- 63), FloatR 0 (- 63)), (1, FloatR 0 (- 37), FloatR 0 (- 37), FloatR 0 (- 37)), (0, FloatR 0 (- 40), FloatR 0 (- 40), FloatR 0 (- 40))])" :: "(real \ real \ real) \ (real \ real \ real) pdevs" Testing conjecture with Quickcheck-narrowing... [1 of 5] Compiling Data_Bits ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Data_Bits.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Data_Bits.o ) [2 of 5] Compiling Typerep ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Typerep.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Typerep.o ) [3 of 5] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Generated_Code.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Generated_Code.o ) [4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Narrowing_Engine.o ) [5 of 5] Compiling Main ( /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Main.hs, /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/Main.o ) Linking /tmp/isabelle-jenkins/process1452954460886564229/Quickcheck_Narrowing5910774/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. *** Failed to load theory "Automatic_Refinement.Refine_Lib" (unresolved "Automatic_Refinement.Misc") *** Failed to load theory "Automatic_Refinement.Autoref_Phases" (unresolved "Automatic_Refinement.Refine_Lib") *** Failed to load theory "Automatic_Refinement.Autoref_Tagging" (unresolved "Automatic_Refinement.Refine_Lib") *** Failed to load theory "Automatic_Refinement.Relators" (unresolved "Automatic_Refinement.Refine_Lib") *** Failed to load theory "Automatic_Refinement.Param_Tool" (unresolved "Automatic_Refinement.Relators") *** Failed to load theory "Automatic_Refinement.Param_HOL" (unresolved "Automatic_Refinement.Param_Tool") *** Failed to load theory "Automatic_Refinement.Parametricity" (unresolved "Automatic_Refinement.Param_HOL", "Automatic_Refinement.Param_Tool") *** Failed to load theory "Automatic_Refinement.Autoref_Id_Ops" (unresolved "Automatic_Refinement.Autoref_Phases", "Automatic_Refinement.Autoref_Tagging", "Automatic_Refinement.Parametricity", "Automatic_Refinement.Refine_Lib") *** Failed to load theory "Automatic_Refinement.Autoref_Fix_Rel" (unresolved "Automatic_Refinement.Autoref_Id_Ops") *** Failed to load theory "Automatic_Refinement.Autoref_Translate" (unresolved "Automatic_Refinement.Autoref_Fix_Rel") *** Failed to load theory "Automatic_Refinement.Autoref_Gen_Algo" (unresolved "Automatic_Refinement.Autoref_Translate") *** Failed to load theory "Automatic_Refinement.Autoref_Relator_Interface" (unresolved "Automatic_Refinement.Autoref_Fix_Rel", "Automatic_Refinement.Autoref_Id_Ops") *** Failed to load theory "Automatic_Refinement.Autoref_Tool" (unresolved "Automatic_Refinement.Autoref_Gen_Algo", "Automatic_Refinement.Autoref_Relator_Interface", "Automatic_Refinement.Autoref_Translate") *** Failed to load theory "Automatic_Refinement.Autoref_Bindings_HOL" (unresolved "Automatic_Refinement.Autoref_Tool") *** Failed to load theory "Automatic_Refinement.Automatic_Refinement" (unresolved "Automatic_Refinement.Autoref_Bindings_HOL", "Automatic_Refinement.Autoref_Tool") *** Failed to load theory "Collections.Intf_Comp" (unresolved "Automatic_Refinement.Automatic_Refinement") *** Failed to load theory "Collections.SetIterator" (unresolved "Automatic_Refinement.Misc") *** Failed to load theory "Collections.Idx_Iterator" (unresolved "Automatic_Refinement.Automatic_Refinement", "Collections.SetIterator") *** Failed to load theory "Collections.SetIteratorOperations" (unresolved "Collections.SetIterator") *** Failed to load theory "Collections.Assoc_List" (unresolved "Collections.SetIteratorOperations") *** Failed to load theory "Collections.Diff_Array" (unresolved "Automatic_Refinement.Parametricity", "Collections.Assoc_List") *** Failed to load theory "Collections.Impl_Array_Stack" (unresolved "Automatic_Refinement.Automatic_Refinement", "Collections.Diff_Array") *** Failed to load theory "Collections.Proper_Iterator" (unresolved "Automatic_Refinement.Refine_Lib", "Collections.SetIteratorOperations") *** Failed to load theory "Collections.It_to_It" (unresolved "Collections.Proper_Iterator") *** Failed to load theory "Collections.SetIteratorGA" (unresolved "Collections.SetIteratorOperations") *** Failed to load theory "Collections.Intf_Hash" (unresolved "Automatic_Refinement.Automatic_Refinement") *** Failed to load theory "Collections.Gen_Hash" (unresolved "Collections.Intf_Hash") *** Failed to load theory "Refine_Monadic.Refine_Mono_Prover" (unresolved "Automatic_Refinement.Refine_Lib") *** Failed to load theory "Refine_Monadic.Refine_Misc" (unresolved "Automatic_Refinement.Automatic_Refinement", "Refine_Monadic.Refine_Mono_Prover") *** Failed to load theory "Refine_Monadic.RefineG_Domain" (unresolved "Refine_Monadic.Refine_Misc") *** Failed to load theory "Refine_Monadic.RefineG_Transfer" (unresolved "Refine_Monadic.Refine_Misc") *** Failed to load theory "Refine_Monadic.RefineG_Assert" (unresolved "Refine_Monadic.RefineG_Transfer") *** Failed to load theory "Refine_Monadic.RefineG_Recursion" (unresolved "Refine_Monadic.RefineG_Domain", "Refine_Monadic.RefineG_Transfer", "Refine_Monadic.Refine_Misc") *** Failed to load theory "Refine_Monadic.RefineG_While" (unresolved "Refine_Monadic.RefineG_Recursion") *** Failed to load theory "Refine_Monadic.Refine_Det" (unresolved "Refine_Monadic.RefineG_Assert", "Refine_Monadic.RefineG_While") *** Failed to load theory "Refine_Monadic.Refine_Basic" (unresolved "Refine_Monadic.RefineG_Assert", "Refine_Monadic.RefineG_Recursion", "Refine_Monadic.Refine_Misc") *** Failed to load theory "Refine_Monadic.Refine_Heuristics" (unresolved "Refine_Monadic.Refine_Basic") *** Failed to load theory "Refine_Monadic.Refine_Leof" (unresolved "Refine_Monadic.Refine_Basic") *** Failed to load theory "Refine_Monadic.Refine_More_Comb" (unresolved "Refine_Monadic.Refine_Basic", "Refine_Monadic.Refine_Heuristics", "Refine_Monadic.Refine_Leof") *** Failed to load theory "Refine_Monadic.Refine_Pfun" (unresolved "Refine_Monadic.Refine_Basic", "Refine_Monadic.Refine_Det") *** Failed to load theory "Refine_Monadic.Refine_While" (unresolved "Refine_Monadic.RefineG_While", "Refine_Monadic.Refine_Basic", "Refine_Monadic.Refine_Leof") *** Failed to load theory "Refine_Monadic.Refine_Transfer" (unresolved "Refine_Monadic.RefineG_Transfer", "Refine_Monadic.Refine_Basic", "Refine_Monadic.Refine_Det", "Refine_Monadic.Refine_While") *** Failed to load theory "Refine_Monadic.Autoref_Monadic" (unresolved "Refine_Monadic.Refine_Transfer") *** Failed to load theory "Refine_Monadic.Refine_Automation" (unresolved "Refine_Monadic.Refine_Basic", "Refine_Monadic.Refine_Transfer") *** Failed to load theory "Refine_Monadic.Refine_Foreach" (unresolved "Refine_Monadic.Refine_Heuristics", "Refine_Monadic.Refine_Pfun", "Refine_Monadic.Refine_Transfer", "Refine_Monadic.Refine_While") *** Failed to load theory "Refine_Monadic.Refine_Monadic" (unresolved "Refine_Monadic.Autoref_Monadic", "Refine_Monadic.Refine_Automation", "Refine_Monadic.Refine_Basic", "Refine_Monadic.Refine_Foreach", "Refine_Monadic.Refine_Heuristics", "Refine_Monadic.Refine_Leof", "Refine_Monadic.Refine_More_Comb", "Refine_Monadic.Refine_Pfun", "Refine_Monadic.Refine_Transfer", "Refine_Monadic.Refine_While") *** Failed to load theory "Collections.Gen_Iterator" (unresolved "Collections.Proper_Iterator", "Refine_Monadic.Refine_Monadic") *** Failed to load theory "Collections.Iterator" (unresolved "Collections.Gen_Iterator", "Collections.Idx_Iterator", "Collections.It_to_It", "Collections.Proper_Iterator", "Collections.SetIteratorGA", "Collections.SetIteratorOperations") *** Failed to load theory "Collections.Array_Iterator" (unresolved "Collections.Diff_Array", "Collections.Iterator") *** Failed to load theory "Collections.RBT_add" (unresolved "Collections.Iterator") *** Failed to load theory "Collections.Intf_Map" (unresolved "Refine_Monadic.Refine_Monadic") *** Failed to load theory "Collections.Gen_Map" (unresolved "Collections.Intf_Map", "Collections.Iterator") *** Failed to load theory "Collections.Impl_Array_Map" (unresolved "Automatic_Refinement.Automatic_Refinement", "Collections.Diff_Array", "Collections.Gen_Map", "Collections.Intf_Comp", "Collections.Intf_Map", "Collections.Iterator") *** Failed to load theory "Collections.Impl_List_Map" (unresolved "Collections.Gen_Map", "Collections.Intf_Comp", "Collections.Intf_Map", "Collections.Iterator") *** Failed to load theory "Collections.Impl_Array_Hash_Map" (unresolved "Automatic_Refinement.Automatic_Refinement", "Collections.Array_Iterator", "Collections.Diff_Array", "Collections.Gen_Map", "Collections.Impl_List_Map", "Collections.Intf_Hash", "Collections.Intf_Map") *** Failed to load theory "Collections.Impl_RBT_Map" (unresolved "Automatic_Refinement.Automatic_Refinement", "Collections.Intf_Comp", "Collections.Intf_Map", "Collections.Iterator", "Collections.RBT_add") *** Failed to load theory "Collections.Intf_Set" (unresolved "Refine_Monadic.Refine_Monadic") *** Failed to load theory "Collections.Gen_Map2Set" (unresolved "Collections.Intf_Comp", "Collections.Intf_Map", "Collections.Intf_Set", "Collections.Iterator") *** Failed to load theory "Collections.Gen_Set" (unresolved "Collections.Intf_Set", "Collections.Iterator") *** Failed to load theory "Collections.Impl_Bit_Set" (unresolved "Collections.Intf_Set", "Collections.Iterator") *** Failed to load theory "Collections.Impl_Cfun_Set" (unresolved "Collections.Intf_Set") *** Failed to load theory "Collections.Impl_List_Set" (unresolved "Collections.Intf_Set", "Collections.Iterator") *** Failed to load theory "Collections.Impl_Uv_Set" (unresolved "Collections.Intf_Set", "Collections.Iterator") *** Failed to load theory "HOL-ODE-Numerics.GenCF_No_Comp" (unresolved "Automatic_Refinement.Refine_Lib", "Collections.Gen_Hash", "Collections.Gen_Map", "Collections.Gen_Map2Set", "Collections.Gen_Set", "Collections.Impl_Array_Hash_Map", "Collections.Impl_Array_Map", "Collections.Impl_Array_Stack", "Collections.Impl_Bit_Set", "Collections.Impl_Cfun_Set", "Collections.Impl_List_Map", "Collections.Impl_List_Set", "Collections.Impl_RBT_Map", "Collections.Impl_Uv_Set") *** Failed to load theory "HOL-ODE-Numerics.Refine_Dflt_No_Comp" (unresolved "HOL-ODE-Numerics.GenCF_No_Comp", "Refine_Monadic.Refine_Monadic") *** Failed to load theory "HOL-ODE-Numerics.Autoref_Misc" (unresolved "HOL-ODE-Numerics.Refine_Dflt_No_Comp") *** Failed to load theory "HOL-ODE-Numerics.Refine_Folds" (unresolved "HOL-ODE-Numerics.Autoref_Misc") *** Failed to load theory "HOL-ODE-Numerics.Refine_String" (unresolved "HOL-ODE-Numerics.Autoref_Misc") *** Failed to load theory "HOL-ODE-Numerics.Weak_Set" (unresolved "HOL-ODE-Numerics.Autoref_Misc") *** Failed to load theory "HOL-ODE-Numerics.Refine_Vector_List" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Weak_Set") *** Failed to load theory "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" (unresolved "HOL-ODE-Numerics.Refine_Vector_List") *** Failed to load theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector") *** Failed to load theory "HOL-ODE-Numerics.Refine_Reachability_Analysis" (unresolved "HOL-ODE-Numerics.Refine_Folds", "HOL-ODE-Numerics.Refine_Rigorous_Numerics", "HOL-ODE-Numerics.Refine_String", "HOL-ODE-Numerics.Weak_Set") *** Failed to load theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" (unresolved "HOL-ODE-Numerics.Refine_Reachability_Analysis", "HOL-ODE-Numerics.Refine_Rigorous_Numerics") *** Failed to load theory "HOL-ODE-Numerics.Example_Utilities" (unresolved "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform", "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector") *** Failed to load theory "HOL-ODE-Numerics.ODE_Numerics" (unresolved "HOL-ODE-Numerics.Example_Utilities", "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform", "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector") *** Type unification failed: Clash of types "_ \ _" and "_ set" *** *** Type error in application: incompatible operand type *** *** Operator: (=) {} :: ??'a set \ bool *** Operand: f ++ g :: ??'b \ ??'c option *** *** At command "lemma" (line 273 of "~~/afp/thys/Automatic_Refinement/Lib/Misc.thy")