Loading theory "HOL-Eisbach.Eisbach" (required by "Automatic_Refinement.Misc") Loading theory "HOL-Library.Cancellation" (required by "Automatic_Refinement.Misc" via "HOL-Library.Multiset") 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 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 structure Eisbach_Rule_Insts: sig end ### ML warning (line 50 of "~~/src/HOL/Library/Cancellation/cancel.ML"): ### Pattern is not exhaustive. signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL signature CANCEL_DATA = sig val dest_coeff: term -> int * term val dest_sum: term -> term list val find_first_coeff: term -> term list -> int * term list val mk_coeff: int * term -> term val mk_sum: typ -> term list -> term val norm_ss1: simpset val norm_ss2: simpset val norm_tac: Proof.context -> tactic val numeral_simp_tac: Proof.context -> tactic val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option val simplify_meta_eq: Proof.context -> thm -> thm val trans_tac: Proof.context -> thm option -> tactic end structure Cancel_Data: CANCEL_DATA ### 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.710s elapsed time, 1.416s cpu time, 0.000s GC time Loading theory "HOL-Library.Infinite_Set" (required by "Automatic_Refinement.Misc") signature CANCEL_SIMPROCS = sig val diff_cancel: Proof.context -> cterm -> thm option val eq_cancel: Proof.context -> cterm -> thm option val less_cancel: Proof.context -> cterm -> thm option val less_eq_cancel: Proof.context -> cterm -> thm option end structure Cancel_Simprocs: CANCEL_SIMPROCS ### theory "HOL-Library.Cancellation" ### 0.735s elapsed time, 1.488s cpu time, 0.000s GC time Loading theory "HOL-Library.Multiset" (required by "Automatic_Refinement.Misc") consts enumerate :: "'a set \ nat \ 'a" ### theory "HOL-Library.Infinite_Set" ### 0.405s elapsed time, 0.892s cpu time, 0.000s GC time Loading theory "HOL-Library.Option_ord" (required by "Automatic_Refinement.Misc") instantiation multiset :: (type) cancel_comm_monoid_add zero_multiset == zero_class.zero :: 'a multiset minus_multiset == minus :: 'a multiset \ 'a multiset \ 'a multiset plus_multiset == plus :: 'a multiset \ 'a multiset \ 'a multiset 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 ### theory "HOL-Library.Option_ord" ### 0.625s elapsed time, 1.224s cpu time, 0.248s GC time Loading theory "IP_Addresses.NumberWang_IPv4" ### theory "IP_Addresses.NumberWang_IPv4" ### 0.046s elapsed time, 0.092s cpu time, 0.000s GC time Loading theory "IP_Addresses.NumberWang_IPv6" ### theory "IP_Addresses.NumberWang_IPv6" ### 0.096s elapsed time, 0.196s cpu time, 0.000s GC time Loading theory "IP_Addresses.Word_More" ### Partially applied constant "Multiset.inf_subset_mset" on left hand side of equation, in theorem: ### semilattice_inf.Inf_fin (\#) (set (?x # ?xs)) \ ### fold (\#) ?xs ?x ### Partially applied constant "Multiset.sup_subset_mset" on left hand side of equation, in theorem: ### semilattice_sup.Sup_fin (\#) (set (?x # ?xs)) \ ### fold (\#) ?xs ?x ### theory "IP_Addresses.Word_More" ### 0.048s elapsed time, 0.096s cpu time, 0.000s GC time Found termination order: "(\p. size (fst p)) <*mlex*> {}" signature MULTISET_SIMPROCS = sig val subset_cancel_msets: Proof.context -> cterm -> thm option val subseteq_cancel_msets: Proof.context -> cterm -> thm option end structure Multiset_Simprocs: MULTISET_SIMPROCS instantiation multiset :: (type) Inf Inf_multiset == Inf :: 'a multiset set \ 'a multiset instantiation multiset :: (type) Sup Sup_multiset == Sup :: 'a multiset set \ 'a multiset instantiation multiset :: (type) size size_multiset == size :: 'a multiset \ nat locale comp_fun_commute fixes f :: "'a \ 'b \ 'b" assumes "comp_fun_commute f" consts mset :: "'a list \ 'a multiset" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" locale comm_monoid_mset fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) and z :: "'a" ("\<^bold>1") assumes "comm_monoid_mset (\<^bold>* ) \<^bold>1" class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" class canonically_ordered_monoid_add = ordered_comm_monoid_add + assumes "le_iff_add": "\a b. (a \ b) = (\c. b = a + c)" class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd + assumes "mult_1": "\a. (1::'a) * a = a" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" instantiation multiset :: (preorder) order less_eq_multiset == less_eq :: 'a multiset \ 'a multiset \ bool less_multiset == less :: 'a multiset \ 'a multiset \ bool instantiation multiset :: (preorder) ordered_ab_semigroup_add Proofs for inductive predicate(s) "pw_leq" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "(\p. length (fst p)) <*mlex*> {}" instantiation multiset :: (equal) equal equal_multiset == equal_class.equal :: 'a multiset \ 'a multiset \ bool instantiation multiset :: (random) random random_multiset == random_class.random :: natural \ natural \ natural \ ('a multiset \ (unit \ term)) \ natural \ natural instantiation multiset :: (full_exhaustive) full_exhaustive full_exhaustive_multiset == full_exhaustive_class.full_exhaustive :: ('a multiset \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option Proofs for inductive predicate(s) "pred_mset" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "rel_mset'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Library.Multiset" ### 5.504s elapsed time, 10.752s cpu time, 0.660s GC time Loading theory "HOL-ex.Quicksort" (required by "Automatic_Refinement.Misc") class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Found termination order: "length <*mlex*> {}" ### theory "HOL-ex.Quicksort" ### 0.652s elapsed time, 1.280s cpu time, 0.292s GC time Loading theory "Automatic_Refinement.Misc" ### theory "Automatic_Refinement.Misc" ### 0.701s elapsed time, 1.408s cpu time, 0.000s GC time ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'h in "A__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'd, 'e in "X__" or "f__" or "g__" ### Introduced fixed type variable(s): 'd, 'e in "f__" ### Introduced fixed type variable(s): 'd in "X__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__" ### Introduced fixed type variable(s): 'd, 'e in "R__" ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Introduced fixed type variable(s): 'd in "z__" ### Introduced fixed type variable(s): 'd in "P__" INFIMUM ?A Sup = SUPREMUM {f ` ?A |f. \Y\?A. f Y \ Y} Inf uint ?a = uint ?b \ ?a = ?b (?a \ ?b) = (unat ?a \ unat ?b) isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IP_Addresses/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/IP_Addresses/outline -o pdf -n outline -t /proof,/ML *** 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")