Loading theory "HOL-Library.Cancellation" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.Multiset") Loading theory "HOL-Library.Infinite_Set" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") consts enumerate :: "'a set \ nat \ 'a" ### theory "HOL-Library.Infinite_Set" ### 0.424s elapsed time, 0.924s cpu time, 0.000s GC time Loading theory "HOL-Library.Nat_Bijection" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.FSet" via "HOL-Library.Countable") ### 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 Found termination order: "(\p. size (snd p)) <*mlex*> {}" 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.748s elapsed time, 1.580s cpu time, 0.000s GC time Loading theory "HOL-Library.Multiset" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") Found termination order: "size_list size <*mlex*> {}" ### theory "HOL-Library.Nat_Bijection" ### 0.564s elapsed time, 1.124s cpu time, 0.000s GC time Loading theory "HOL-Library.Old_Datatype" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.FSet" via "HOL-Library.Countable") 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 signature OLD_DATATYPE = sig val check_specs: spec list -> theory -> spec list * Proof.context type config = {quiet: bool, strict: bool} val default_config: config type descr = (int * (string * dtyp list * (string * dtyp list) list)) list val distinct_lemma: thm datatype dtyp = DtRec of int | DtTFree of string * sort | DtType of string * dtyp list type info = {case_cong: thm, case_cong_weak: thm, case_name: string, case_rewrites: thm list, descr: descr, distinct: thm list, exhaust: thm, index: int, induct: thm, inducts: thm list, inject: thm list, nchotomy: thm, rec_names: string list, rec_rewrites: thm list, split: thm, split_asm: thm} val read_specs: spec_cmd list -> theory -> spec list * Proof.context type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list type spec_cmd = (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list end structure Old_Datatype: OLD_DATATYPE ### theory "HOL-Library.Old_Datatype" ### 0.969s elapsed time, 1.900s cpu time, 0.436s GC time Loading theory "HOL-Library.Phantom_Type" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "FinFun.FinFun" via "HOL-Library.Cardinality") ### 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 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 ### theory "HOL-Library.Phantom_Type" ### 0.782s elapsed time, 1.576s cpu time, 0.000s GC time Loading theory "HOL-Library.Cardinality" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "FinFun.FinFun") instantiation multiset :: (type) size size_multiset == size :: 'a multiset \ nat ### Additional type variable(s) in locale specification "card2": 'a class card2 = finite + assumes "two_le_card": "2 \ CARD('a)" locale comp_fun_commute fixes f :: "'a \ 'b \ 'b" assumes "comp_fun_commute f" class finite_UNIV = type + fixes finite_UNIV :: "('a, bool) phantom" assumes "finite_UNIV": "finite_UNIV = Phantom('a) (finite UNIV)" class card_UNIV = finite_UNIV + fixes card_UNIV :: "('a, nat) phantom" assumes "card_UNIV": "card_UNIV_class.card_UNIV = Phantom('a) CARD('a)" instantiation nat :: card_UNIV card_UNIV_nat == card_UNIV_class.card_UNIV :: (nat, nat) phantom finite_UNIV_nat == finite_UNIV :: (nat, bool) phantom instantiation int :: card_UNIV card_UNIV_int == card_UNIV_class.card_UNIV :: (int, nat) phantom finite_UNIV_int == finite_UNIV :: (int, bool) phantom instantiation natural :: card_UNIV card_UNIV_natural == card_UNIV_class.card_UNIV :: (natural, nat) phantom finite_UNIV_natural == finite_UNIV :: (natural, bool) phantom instantiation integer :: card_UNIV card_UNIV_integer == card_UNIV_class.card_UNIV :: (integer, nat) phantom finite_UNIV_integer == finite_UNIV :: (integer, bool) phantom consts mset :: "'a list \ 'a multiset" instantiation list :: (type) card_UNIV card_UNIV_list == card_UNIV_class.card_UNIV :: ('a list, nat) phantom finite_UNIV_list == finite_UNIV :: ('a list, bool) phantom instantiation unit :: card_UNIV card_UNIV_unit == card_UNIV_class.card_UNIV :: (unit, nat) phantom finite_UNIV_unit == finite_UNIV :: (unit, bool) phantom instantiation bool :: card_UNIV card_UNIV_bool == card_UNIV_class.card_UNIV :: (bool, nat) phantom finite_UNIV_bool == finite_UNIV :: (bool, bool) phantom instantiation char :: card_UNIV card_UNIV_char == card_UNIV_class.card_UNIV :: (char, nat) phantom finite_UNIV_char == finite_UNIV :: (char, bool) phantom instantiation prod :: (finite_UNIV, finite_UNIV) finite_UNIV finite_UNIV_prod == finite_UNIV :: ('a \ 'b, bool) phantom instantiation prod :: (card_UNIV, card_UNIV) card_UNIV card_UNIV_prod == card_UNIV_class.card_UNIV :: ('a \ 'b, nat) phantom instantiation sum :: (finite_UNIV, finite_UNIV) finite_UNIV finite_UNIV_sum == finite_UNIV :: ('a + 'b, bool) phantom instantiation sum :: (card_UNIV, card_UNIV) card_UNIV card_UNIV_sum == card_UNIV_class.card_UNIV :: ('a + 'b, nat) phantom instantiation fun :: (finite_UNIV, card_UNIV) finite_UNIV finite_UNIV_fun == finite_UNIV :: ('a \ 'b, bool) phantom instantiation fun :: (card_UNIV, card_UNIV) card_UNIV card_UNIV_fun == card_UNIV_class.card_UNIV :: ('a \ 'b, nat) phantom instantiation option :: (finite_UNIV) finite_UNIV finite_UNIV_option == finite_UNIV :: ('a option, bool) phantom instantiation option :: (card_UNIV) card_UNIV card_UNIV_option == card_UNIV_class.card_UNIV :: ('a option, nat) phantom instantiation String.literal :: card_UNIV card_UNIV_literal == card_UNIV_class.card_UNIV :: (String.literal, nat) phantom finite_UNIV_literal == finite_UNIV :: (String.literal, bool) phantom instantiation set :: (finite_UNIV) finite_UNIV finite_UNIV_set == finite_UNIV :: ('a set, bool) phantom class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" instantiation set :: (card_UNIV) card_UNIV card_UNIV_set == card_UNIV_class.card_UNIV :: ('a set, nat) phantom instantiation Enum.finite_1 :: card_UNIV card_UNIV_finite_1 == card_UNIV_class.card_UNIV :: (Enum.finite_1, nat) phantom finite_UNIV_finite_1 == finite_UNIV :: (Enum.finite_1, bool) phantom instantiation Enum.finite_2 :: card_UNIV card_UNIV_finite_2 == card_UNIV_class.card_UNIV :: (Enum.finite_2, nat) phantom finite_UNIV_finite_2 == finite_UNIV :: (Enum.finite_2, bool) phantom instantiation Enum.finite_3 :: card_UNIV card_UNIV_finite_3 == card_UNIV_class.card_UNIV :: (Enum.finite_3, nat) phantom finite_UNIV_finite_3 == finite_UNIV :: (Enum.finite_3, bool) phantom instantiation Enum.finite_4 :: card_UNIV card_UNIV_finite_4 == card_UNIV_class.card_UNIV :: (Enum.finite_4, nat) phantom finite_UNIV_finite_4 == finite_UNIV :: (Enum.finite_4, bool) phantom instantiation Enum.finite_5 :: card_UNIV card_UNIV_finite_5 == card_UNIV_class.card_UNIV :: (Enum.finite_5, nat) phantom finite_UNIV_finite_5 == finite_UNIV :: (Enum.finite_5, bool) phantom 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" ### Code generator: dropping subsumed code equation ### List.coset [] \ set [] \ False 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)" ### theory "HOL-Library.Cardinality" ### 1.091s elapsed time, 2.184s cpu time, 0.000s GC time Loading theory "FinFun.FinFun" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") ### theory "FinFun.FinFun" ### 0.103s elapsed time, 0.204s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Syntax" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List" via "HOL-Library.Quotient_Set") ### theory "HOL-Library.Quotient_Syntax" ### 0.026s elapsed time, 0.052s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Option" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List") ### theory "HOL-Library.Quotient_Option" ### 0.079s elapsed time, 0.160s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Product" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List") class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd + assumes "mult_1": "\a. (1::'a) * a = a" ### theory "HOL-Library.Quotient_Product" ### 0.143s elapsed time, 0.288s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Set" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List") ### theory "HOL-Library.Quotient_Set" ### 0.110s elapsed time, 0.220s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_List" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs") class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "HOL-Library.Quotient_List" ### 0.469s elapsed time, 0.932s cpu time, 0.000s GC time Loading theory "HOL-Library.Countable" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.FSet") 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 ... ### Additional type variable(s) in locale specification "countable": 'a class countable = type + assumes "ex_inj": "\to_nat. inj to_nat" Proofs for inductive predicate(s) "finite_item" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... 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 val old_countable_datatype_tac = fn: Proof.context -> int -> tactic ### ML warning (line 93 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 139 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 143 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 145 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 156 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. signature BNF_LFP_COUNTABLE = sig val countable_datatype_tac: Proof.context -> tactic val derive_encode_injectives_thms: Proof.context -> string list -> thm list end structure BNF_LFP_Countable: BNF_LFP_COUNTABLE val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq val countable_tac = fn: Proof.context -> int -> tactic 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 ... ### theory "HOL-Library.Countable" ### 1.912s elapsed time, 3.772s cpu time, 0.804s GC time Loading theory "HOL-Library.FSet" (required by "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") 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 ... instantiation fset :: (finite) finite instantiation fset :: (type) {minus,bounded_lattice_bot,distrib_lattice} inf_fset == inf :: 'a fset \ 'a fset \ 'a fset bot_fset == bot :: 'a fset sup_fset == sup :: 'a fset \ 'a fset \ 'a fset less_eq_fset == less_eq :: 'a fset \ 'a fset \ bool less_fset == less :: 'a fset \ 'a fset \ bool minus_fset == minus :: 'a fset \ 'a fset \ 'a fset ### theory "HOL-Library.Multiset" ### 6.131s elapsed time, 12.172s cpu time, 1.240s GC time instantiation fset :: (equal) equal equal_fset == equal_class.equal :: 'a fset \ 'a fset \ bool instantiation fset :: (type) conditionally_complete_lattice Inf_fset == Inf :: 'a fset set \ 'a fset Sup_fset == Sup :: 'a fset set \ 'a fset instantiation fset :: (finite) complete_lattice top_fset == top :: 'a fset instantiation fset :: (finite) complete_boolean_algebra uminus_fset == uminus :: 'a fset \ 'a fset locale comp_fun_commute fixes f :: "'a \ 'b \ 'b" assumes "comp_fun_commute f" locale comp_fun_idem fixes f :: "'a \ 'b \ 'b" assumes "comp_fun_idem f" locale comm_monoid_fset fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) and z :: "'a" ("\<^bold>1") assumes "comm_monoid_fset (\<^bold>* ) \<^bold>1" class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" locale semilattice_fset fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) assumes "semilattice_fset (\<^bold>* )" locale semilattice_order_fset fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) and less_eq :: "'a \ 'a \ bool" (infix "\<^bold>\" 50) and less :: "'a \ 'a \ bool" (infix "\<^bold><" 50) assumes "semilattice_order_fset (\<^bold>* ) (\<^bold>\) (\<^bold><)" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" instantiation fset :: (type) size size_fset == size :: 'a fset \ nat instantiation fset :: (exhaustive) exhaustive exhaustive_fset == exhaustive_class.exhaustive :: ('a fset \ (bool \ term list) option) \ natural \ (bool \ term list) option Found termination order: "(\p. nat_of_natural (snd p)) <*mlex*> {}" instantiation fset :: (full_exhaustive) full_exhaustive full_exhaustive_fset == full_exhaustive_class.full_exhaustive :: ('a fset \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option Found termination order: "(\p. nat_of_natural (snd p)) <*mlex*> {}" instantiation fset :: (random) random random_fset == random_class.random :: natural \ natural \ natural \ ('a fset \ (unit \ term)) \ natural \ natural ### Additional type variable(s) in specification of "random_aux_fset_rel": 'a ### Additional type variable(s) in specification of "random_aux_fset_dom": 'a Found termination order: "(\p. nat_of_natural (fst p)) <*mlex*> {}" ### theory "HOL-Library.FSet" ### 4.802s elapsed time, 9.552s cpu time, 0.852s GC time ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'h in "A__" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Introduced fixed type variable(s): 'b in "xs__" or "ys__" ### 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__" isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nominal2/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Nominal2/outline -o pdf -n outline -t /proof,/ML *** Failed to load theory "Nominal2.Nominal2_Base" (unresolved "FinFun.FinFun") *** Failed to load theory "Nominal2.Atoms" (unresolved "Nominal2.Nominal2_Base") *** Failed to load theory "Nominal2.Eqvt" (unresolved "Nominal2.Nominal2_Base") *** Failed to load theory "Nominal2.Nominal2_Abs" (unresolved "Nominal2.Nominal2_Base") *** Failed to load theory "Nominal2.Nominal2_FCB" (unresolved "Nominal2.Nominal2_Abs") *** Failed to load theory "Nominal2.Nominal2" (unresolved "Nominal2.Nominal2_Abs", "Nominal2.Nominal2_Base", "Nominal2.Nominal2_FCB") *** Type unification failed: Clash of types "_ set" and "_ \ _" *** *** Type error in application: incompatible operand type *** *** Operator: map_default b :: *** (??'a \ ??'b option) \ ??'a \ ??'b *** Operand: {} :: ??'c set *** *** At command "lemma" (line 33 of "~~/afp/thys/FinFun/FinFun.thy")