Loading theory "HOL-Library.Cancellation" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.Multiset") Loading theory "HOL-Library.Infinite_Set" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") Loading theory "HOL-Library.Nat_Bijection" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.FSet" via "HOL-Library.Countable") Loading theory "HOL-Library.Old_Datatype" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.FSet" via "HOL-Library.Countable") Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "size_list size <*mlex*> {}" ### theory "HOL-Library.Infinite_Set" ### 0.440s elapsed time, 1.808s cpu time, 0.000s GC time Loading theory "HOL-Library.Phantom_Type" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "FinFun.FinFun" via "HOL-Library.Cardinality") signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL ### theory "HOL-Library.Nat_Bijection" ### 0.508s elapsed time, 2.088s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Syntax" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List" via "HOL-Library.Quotient_Set") 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 ### theory "HOL-Library.Quotient_Syntax" ### 0.036s elapsed time, 0.144s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Option" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List") ### theory "HOL-Library.Quotient_Option" ### 0.081s elapsed time, 0.324s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Product" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List") 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.674s elapsed time, 2.764s cpu time, 0.000s GC time Loading theory "HOL-Library.Multiset" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") 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.694s elapsed time, 2.832s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_Set" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs" via "HOL-Library.Quotient_List") ### theory "HOL-Library.Quotient_Product" ### 0.139s elapsed time, 0.556s cpu time, 0.000s GC time Loading theory "HOL-Library.Countable" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "HOL-Library.FSet") ### theory "HOL-Library.Quotient_Set" ### 0.108s elapsed time, 0.432s cpu time, 0.000s GC time Loading theory "HOL-Library.Quotient_List" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Abs") ### theory "HOL-Library.Quotient_List" ### 0.544s elapsed time, 2.152s cpu time, 0.456s GC time ### Additional type variable(s) in locale specification "countable": 'a ### theory "HOL-Library.Phantom_Type" ### 0.977s elapsed time, 3.892s cpu time, 0.456s GC time Loading theory "HOL-Library.Cardinality" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base" via "FinFun.FinFun") ### Additional type variable(s) in locale specification "CARD_1": 'a 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 ... ### 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 ### Additional type variable(s) in locale specification "card2": 'a val old_countable_datatype_tac = fn: Proof.context -> int -> tactic Found termination order: "(\p. size (fst p)) <*mlex*> {}" ### 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 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 ### theory "HOL-Library.Countable" ### 1.587s elapsed time, 6.368s cpu time, 0.456s GC time Loading theory "HOL-Library.FSet" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") ### Code generator: dropping subsumed code equation ### List.coset [] \ set [] \ False ### theory "HOL-Library.Cardinality" ### 1.297s elapsed time, 5.196s cpu time, 0.000s GC time Loading theory "FinFun.FinFun" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2" via "Nominal2.Nominal2_Base") 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*> {}" ### theory "FinFun.FinFun" ### 3.075s elapsed time, 12.200s cpu time, 1.280s GC time 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 ... Found termination order: "(\p. nat_of_natural (snd p)) <*mlex*> {}" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### theory "HOL-Library.Multiset" ### 5.449s elapsed time, 21.688s cpu time, 1.736s GC time Found termination order: "(\p. nat_of_natural (snd p)) <*mlex*> {}" ### Introduced fixed type variable(s): 'b in "xs__" or "ys__" ### Metis: Unused theorems: "??.unknown" ### 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.193s elapsed time, 16.688s cpu time, 1.280s GC time Loading theory "Nominal2.Nominal2_Base" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2") ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'h in "A__" ### ML warning (line 76 of "$AFP/Nominal2/nominal_basics.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 94 of "$AFP/Nominal2/nominal_basics.ML"): ### Value identifier (eq) has not been referenced. ### ML warning (line 116 of "$AFP/Nominal2/nominal_basics.ML"): ### Matches are not exhaustive. ### ML warning (line 119 of "$AFP/Nominal2/nominal_basics.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 131 of "$AFP/Nominal2/nominal_basics.ML"): ### Value identifier (z) has not been referenced. ### ML warning (line 131 of "$AFP/Nominal2/nominal_basics.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 130 of "$AFP/Nominal2/nominal_basics.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 156 of "$AFP/Nominal2/nominal_basics.ML"): ### Pattern is not exhaustive. infix 1 ||>>> infix 1 |>>> signature NOMINAL_BASIC = sig val case_sum_const: typ -> typ -> typ -> term val dest_fsetT: typ -> typ val dest_listT: typ -> typ val dest_perm: term -> term * term val fixed_nonfixed_args: Proof.context -> term -> term * term list val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a val is_fixed: Proof.context -> term -> bool val is_true: term -> bool val last2: 'a list -> 'a * 'a val long_name: Proof.context -> string -> string val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list val mk_All: string * typ -> term -> term val mk_all: string * typ -> term -> term val mk_case_sum: term -> term -> term val mk_equiv: thm -> thm val mk_exists: string * typ -> term -> term val mk_id: term -> term val mk_minus: term -> term val mk_perm: term -> term -> term val mk_perm_ty: typ -> term -> term -> term val mk_plus: term -> term -> term val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list val perm_const: typ -> term val perm_ty: typ -> typ val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list val safe_mk_equiv: thm -> thm val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list val split_last2: 'a list -> 'a list * 'a * 'a val split_triples: ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val trace: bool ref val trace_msg: (unit -> string) -> unit val |>>> : 'a * ('a -> 'b * 'c) -> 'b list * 'c val ||>>> : ('a list * 'b) * ('b -> 'a * 'b) -> 'a list * 'b end structure Nominal_Basic: NOMINAL_BASIC val order = fn: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list val dest_listT = fn: typ -> typ val mk_perm = fn: term -> term -> term val mk_plus = fn: term -> term -> term val split_filter = fn: ('a -> bool) -> 'a list -> 'a list * 'a list val fold_left = fn: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a val split_last2 = fn: 'a list -> 'a list * 'a * 'a val order_default = fn: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list val perm_const = fn: typ -> term val last2 = fn: 'a list -> 'a * 'a val mk_perm_ty = fn: typ -> term -> term -> term val case_sum_const = fn: typ -> typ -> typ -> term val is_fixed = fn: Proof.context -> term -> bool val mk_id = fn: term -> term val mk_All = fn: string * typ -> term -> term val map4 = fn: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list val is_true = fn: term -> bool val safe_mk_equiv = fn: thm -> thm val trace = ref false: bool ref val mk_all = fn: string * typ -> term -> term val mk_case_sum = fn: term -> term -> term val dest_fsetT = fn: typ -> typ val remove_dups = fn: ('a * 'a -> bool) -> 'a list -> 'a list val fixed_nonfixed_args = fn: Proof.context -> term -> term * term list val |>>> = fn: 'a * ('a -> 'b * 'c) -> 'b list * 'c val dest_perm = fn: term -> term * term val mk_equiv = fn: thm -> thm val perm_ty = fn: typ -> typ val mk_exists = fn: string * typ -> term -> term val long_name = fn: Proof.context -> string -> string val split_triples = fn: ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val mk_minus = fn: term -> term val ||>>> = fn: ('a list * 'b) * ('b -> 'a * 'b) -> 'a list * 'b val trace_msg = fn: (unit -> string) -> unit ### ML warning (line 198 of "$AFP/Nominal2/nominal_thmdecls.ML"): ### Pattern is not exhaustive. ### ML warning (line 198 of "$AFP/Nominal2/nominal_thmdecls.ML"): ### Value identifier (p') has not been referenced. ### ML warning (line 239 of "$AFP/Nominal2/nominal_thmdecls.ML"): ### Pattern is not exhaustive. signature NOMINAL_THMDECLS = sig val eqvt_add: attribute val eqvt_del: attribute val eqvt_raw_add: attribute val eqvt_raw_del: attribute val eqvt_transform: Proof.context -> thm -> thm val get_eqvts_raw_thms: Proof.context -> thm list val get_eqvts_thms: Proof.context -> thm list val is_eqvt: Proof.context -> term -> bool end structure Nominal_ThmDecls: NOMINAL_THMDECLS ### ML warning (line 72 of "$AFP/Nominal2/nominal_permeq.ML"): ### Value identifier (pre_thms) has not been referenced. ### ML warning (line 78 of "$AFP/Nominal2/nominal_permeq.ML"): ### Value identifier (post_thms) has not been referenced. infix 4 addpres infix 4 addposts infix 4 addexcls signature NOMINAL_PERMEQ = sig val addexcls: eqvt_config * string list -> eqvt_config val addposts: eqvt_config * thm list -> eqvt_config val addpres: eqvt_config * thm list -> eqvt_config val args_parser: (thm list * string list) context_parser val delposts: eqvt_config -> eqvt_config val delpres: eqvt_config -> eqvt_config datatype eqvt_config = Eqvt_Config of {excluded: string list, post_thms: thm list, pre_thms: thm list, strict_mode: bool} val eqvt_conv: Proof.context -> eqvt_config -> conv val eqvt_relaxed_config: eqvt_config val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm val eqvt_strict_config: eqvt_config val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic val perm_simp_meth: thm list * string list -> Proof.context -> Proof.method val perm_strict_simp_meth: thm list * string list -> Proof.context -> Proof.method val trace_eqvt: bool Config.T end structure Nominal_Permeq: NOMINAL_PERMEQ ### Introduced fixed type variable(s): 'd in "c__" ### Introduced fixed type variable(s): 'c, 'd in "a__" or "b__" or "g__" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Introduced fixed type variable(s): 'e in "a__" or "g'__" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Introduced fixed type variable(s): 'd in "c__" ### Introduced fixed type variable(s): 'd in "b__" or "g'__" ### Introduced fixed type variable(s): 'f in "c__" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Introduced fixed type variable(s): 'd, 'e in "a__" or "fa__" ### Ignoring duplicate rewrite rule: ### ?f1 \ finfun \ curry ?f1 \ finfun \ True ### Ignoring duplicate rewrite rule: ### ?f1 \ finfun \ curry ?f1 ?a1 \ finfun \ True ### Introduced fixed type variable(s): 'g in "b__" or "g__" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ \ (THE x. ?P x) = ?a ### ML warning (line 280 of "$AFP/Nominal2/nominal_library.ML"): ### Value identifier (tys) has not been referenced. ### ML warning (line 279 of "$AFP/Nominal2/nominal_library.ML"): ### Value identifier (tys) has not been referenced. ### ML warning (line 278 of "$AFP/Nominal2/nominal_library.ML"): ### Value identifier (tys) has not been referenced. ### ML warning (line 277 of "$AFP/Nominal2/nominal_library.ML"): ### Value identifier (tys) has not been referenced. type cns_info = (term * typ * typ list * bool list) list signature NOMINAL_LIBRARY = sig val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list val atom_const: typ -> term val atom_ty: typ -> typ val atomify: Proof.context -> term -> term val atomify_ty: Proof.context -> typ -> term -> term val atomize: Proof.context -> thm -> thm val atomize_concl: Proof.context -> thm -> thm val atomize_rule: Proof.context -> int -> thm -> thm type cns_info = (term * typ * typ list * bool list) list val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic val finite_const: typ -> term val fold_append: term list -> term val fold_conj: term list -> term val fold_conj_balanced: term list -> term val fold_union: term list -> term val fold_union_env: typ list -> term list -> term val fresh_args: Proof.context -> term -> term list val fresh_const: typ -> term val fresh_star_const: typ -> term val fresh_star_ty: typ -> typ val fresh_ty: typ -> typ val is_atom: Proof.context -> typ -> bool val is_atom_fset: Proof.context -> typ -> bool val is_atom_list: Proof.context -> typ -> bool val is_atom_set: Proof.context -> typ -> bool val listify: Proof.context -> term -> term val listify_ty: Proof.context -> typ -> term -> term val mk_append: term * term -> term val mk_atom: term -> term val mk_atom_fset: term -> term val mk_atom_fset_ty: typ -> term -> term val mk_atom_list: term -> term val mk_atom_list_ty: typ -> term -> term val mk_atom_set: term -> term val mk_atom_set_ty: typ -> term -> term val mk_atom_ty: typ -> term -> term val mk_binop_env: typ list -> string -> term * term -> term val mk_conj: term * term -> term val mk_diff: term * term -> term val mk_finite: term -> term val mk_finite_ty: typ -> term -> term val mk_fresh: term -> term -> term val mk_fresh_star: term -> term -> term val mk_fresh_star_ty: typ -> term -> term -> term val mk_fresh_ty: typ -> term -> term -> term val mk_full_horn: (string * typ) list -> term list -> term -> term val mk_sort_of: term -> term val mk_supp: term -> term val mk_supp_rel: term -> term -> term val mk_supp_rel_ty: typ -> term -> term -> term val mk_supp_ty: typ -> term -> term val mk_supports: term -> term -> term val mk_supports_ty: typ -> term -> term -> term val mk_union: term * term -> term val mk_union_env: typ list -> term * term -> term val pat_completeness_simp: thm list -> Proof.context -> tactic val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory val prove_termination_ind: Proof.context -> int -> tactic val setify: Proof.context -> term -> term val setify_ty: Proof.context -> typ -> term -> term val size_ss: simpset val strip_full_horn: term -> (string * typ) list * term list * term val supp_const: typ -> term val supp_rel_const: typ -> term val supp_rel_ty: typ -> typ val supp_ty: typ -> typ val supports_const: typ -> term val to_set: term -> term val to_set_ty: typ -> term -> term val transform_prem1: Proof.context -> string list -> thm -> thm val transform_prem2: Proof.context -> string list -> thm -> thm end structure Nominal_Library: NOMINAL_LIBRARY val conj_tac = fn: Proof.context -> (int -> tactic) -> int -> tactic val is_atom_fset = fn: Proof.context -> typ -> bool val mk_union_env = fn: typ list -> term * term -> term val size_ss = Simpset ({depth = (0, ref false), prems = [], rules = Net {atoms = {}, comb = Net {atoms = {("HOL.Ex", Net {atoms = {}, comb = Net {atoms = {("HOL.eq", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "... ...", extra = false, fo = true, lhs = Const ("...", ...) $ Abs ("...", "?'d1", ...), name = "HOL.simp_thms_38", ...}]})}, comb = Leaf [], var = Leaf []}, var = Leaf [{elhs = "\x. ?t1 = x \ ?P1 x", extra = false, fo = false, lhs = Const ("HOL.Ex", "(... ... ...) \ bool") $ Abs ("x", "?'d1", Const ("...", ...) $ (... $ ... $ ...) $ ...), name = "HOL.simp_thms_40", perm = false, thm = "\x. ?t1 ... x \ ?P1 x \ ?P1 ?t1"}, {elhs = "\x. x = ?t1 \ ?P1 x", extra = false, fo = false, lhs = Const ("HOL.Ex", "(...) ... bool") $ Abs ("x", "?'d1", Const ("...", "bool \ bool \ bool") $ ... $ ...), name = "HOL.simp_thms_39", perm = false, thm = "\x. ... ... ... ... ... ... \ ?P1 ?t1"}, {elhs = "\x. x = ?t1", extra = false, fo = true, lhs = Const ("HOL.Ex", "... ... ...") $ Abs ("x", "...", ... $ ... $ ...), name = "HOL.simp_thms_37", perm = false, thm = "...x... ... ... ... \ True"}, {elhs = "\x. ?y", extra = false, fo = true, lhs = Const ("HOL.Ex", "...") $ Abs ("x", "...", ...), name = "HOL.simp_thms_36", perm = false, thm = "......... ... ... ?y"}, {elhs = "...x... ... ... ...", extra = false, fo = false, lhs = Const ("HOL.Ex", "...") $ Abs ("x", ..., ...), name = "HOL.ex_simps_6", perm = false, thm = "... ... ..."}, {elhs = "......... ...", extra = false, fo = false, lhs = Const ("...", ...) $ Abs ("...", "?'e1", ...), name = "HOL.ex_simps_5", ...}, {elhs = "...", extra = false, fo = false, lhs = Const ("...", "(?'d1 \ bool) \ bool") $ ..., ...}, {elhs = "...", extra = false, fo = false, ...}, {elhs = ..., extra = false, ...}, ...]}), ("HOL.All", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "\x. ?t1 \ x", extra = false, fo = true, lhs = Const ("HOL.All", "(...) ... bool") $ Abs ("x", "?'d1", Const ("...", "bool \ bool") $ ...), name = "HOL.simp_thms_44", perm = false, thm = "\x. ?t1 ... x \ False"}, {elhs = "\x. x \ ?t1", extra = false, fo = true, lhs = Const ("HOL.All", "... ... ...") $ Abs ("x", "...", ... $ ...), name = "HOL.simp_thms_43", perm = false, thm = "...x... ... ... ... \ False"}, {elhs = "\x. ... ... ... ... ... ...", extra = false, fo = false, lhs = Const ("HOL.All", "...") $ Abs ("x", "...", ...), name = "HOL.simp_thms_42", perm = false, thm = "......... ... ... ... ..."}, {elhs = "...x... ... ... ...", extra = false, fo = false, lhs = Const ("HOL.All", "...") $ Abs ("x", ..., ...), name = "HOL.simp_thms_41", perm = false, thm = "... ... ..."}, {elhs = "......... ...", extra = false, fo = true, lhs = Const ("...", ...) $ Abs ("...", "?'b1", ...), name = "HOL.simp_thms_35", ...}, {elhs = "...", extra = false, fo = false, lhs = Const ("...", "(?'f1 \ bool) \ bool") $ ..., ...}, {elhs = "...", extra = false, fo = false, ...}, {elhs = ..., extra = false, ...}, ...]}), ("HOL.Not", Net {atoms = {("HOL.True", Leaf [{elhs = "\ True", extra = false, fo = true, lhs = Const ("HOL.Not", "...") $ Const ("HOL.True", "..."), name = "HOL.simp_thms_7", perm = false, thm = "... True ... False"}]), ("HOL.False", Leaf [{elhs = "\ False", extra = false, fo = true, lhs = Const ("HOL.Not", "...") $ Const ("...", ...), name = "HOL.simp_thms_8", perm = false, thm = "... ... ... ..."}])}, comb = Net {atoms = {("HOL.Ex", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "...", extra = false, fo = true, ...}]}), ("HOL.All", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = ..., extra = false, ...}]}), ("HOL.Not", Net {atoms = {}, comb = Leaf [...], var = Leaf [...]})}, comb = Net {atoms = {("HOL.eq", Net {atoms = {}, comb = Leaf [...], var = Net {atoms = {}, ...}}), ("HOL.conj", Net {atoms = {}, comb = ..., var = ...}), ("HOL.disj", Net {atoms = {}, ...}), ("HOL.implies", ...)}, comb = Leaf [], var = Leaf []}, var = Leaf []}, var = Leaf []}), ("HOL.The", Net {atoms = {}, comb = Net {atoms = {("HOL.eq", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = ..., extra = false, ...}]})}, comb = Leaf [], var = Leaf []}, var = Leaf [{elhs = "THE x. x ... ?y", extra = false, fo = true, lhs = Const ("HOL.The", "...") $ Abs ("x", "...", ...), name = "HOL.the_eq_trivial", perm = false, thm = "... ...... ... ... ?y"}]}), ("Pure.all", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "...x... ... ... ... ...", extra = false, fo = false, lhs = Const ("Pure.all", "...") $ Abs ("x", ..., ...), name = "HOL.subst_all_2", perm = false, thm = "... ... ... ..."}, {elhs = "......... ...", extra = false, fo = false, lhs = Const ("...", ...) $ Abs ("...", "?'a", ...), name = "HOL.subst_all_1", ...}, {elhs = "...", extra = false, fo = true, lhs = Const ("...", "(?'a \ prop) \ prop") $ ..., ...}]}), ("Wellfounded.wf", Net {atoms = {}, comb = Net {atoms = {("Wellfounded.measure", Net {atoms = {}, comb = ..., var = ...})}, comb = Leaf [], var = Leaf []}, var = Leaf []})}, comb = Net {atoms = {("HOL.eq", Net {atoms = {("HOL.True", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "... ... ...", extra = false, fo = true, lhs = Const ("...", ...) $ Const ("...", "bool") $ ..., name = "HOL.simp_thms_11", ...}]}), ("HOL.False", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "...", extra = false, fo = true, lhs = Const ("...", "bool \ bool \ bool") $ ... $ ..., ...}]})}, comb = Net {atoms = {("HOL.Not", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Net {atoms = {...}, ...}, var = Leaf [...]}})}, comb = Leaf [], var = Leaf []}, var = Net {atoms = {("HOL.True", Leaf [{elhs = "... ... ...", extra = false, fo = true, lhs = Const ("...", ...) $ Var ((...), "bool") $ ..., name = "HOL.simp_thms_12", ...}]), ("HOL.False", Leaf [{elhs = "...", extra = false, fo = true, lhs = Const ("...", "bool \ bool \ bool") $ ... $ ..., ...}])}, comb = Net {atoms = {("HOL.Not", Net {atoms = {}, comb = Leaf [...], var = Leaf [...]})}, comb = Leaf [], var = Leaf []}, var = Leaf [{elhs = "?x1 ... ?x1", extra = false, fo = true, lhs = Const ("HOL.eq", "...") $ Var (("...", 1), ...) $ Var ((...), "?'a1"), name = "HOL.simp_thms_6", perm = false, thm = "... ... ..."}]}}), ("HOL.conj", Net {atoms = {("HOL.True", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "...", extra = false, fo = true, lhs = Const ("...", "bool \ bool \ bool") $ ... $ ..., ...}]}), ("HOL.False", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "...", extra = false, fo = true, ...}]})}, comb = Net {atoms = {("HOL.Not", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = ..., var = ...}})}, comb = Net {atoms = {("HOL.conj", Net {atoms = {}, comb = ..., var = ...}), ("HOL.implies", Net {atoms = {}, ...})}, comb = Leaf [], var = Leaf []}, var = Leaf []}, var = Net {atoms = {("HOL.True", Leaf [{elhs = "...", extra = false, fo = true, lhs = Const ("...", "bool \ bool \ bool") $ ... $ ..., ...}]), ("HOL.False", Leaf [{elhs = "...", extra = false, fo = true, ...}])}, comb = Net {atoms = {("HOL.Not", Net {atoms = {}, comb = ..., var = ...})}, comb = Net {atoms = {("HOL.conj", ...)}, comb = Leaf [...], var = Leaf [...]}, var = Leaf []}, var = Leaf [{elhs = "... ... ...", extra = false, fo = true, lhs = Const ("...", ...) $ Var ((...), "bool") $ ..., name = "HOL.simp_thms_25", ...}]}}), ("HOL.disj", Net {atoms = {("HOL.True", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = "...", extra = false, fo = true, ...}]}), ("HOL.False", Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = ..., extra = false, ...}]})}, comb = Net {atoms = {("HOL.Not", Net {atoms = {}, comb = Leaf [...], var = Net {atoms = {}, ...}})}, comb = Net {atoms = {("HOL.disj", Net {atoms = {}, ...}), ("HOL.implies", ...)}, comb = Leaf [], var = Leaf []}, var = Leaf []}, var = Net {atoms = {("HOL.True", Leaf [{elhs = "...", extra = false, fo = true, ...}]), ("HOL.False", Leaf [{elhs = ..., extra = false, ...}])}, comb = Net {atoms = {("HOL.Not", Net {atoms = {}, ...})}, comb = Net {atoms = {...}, comb = ..., var = ...}, var = Leaf []}, var = Leaf [{elhs = "...", extra = false, fo = true, lhs = Const ("...", "bool \ bool \ bool") $ ... $ ..., ...}]}}), ("Pure.imp", Net {atoms = {}, comb = Net {atoms = {("HOL.Trueprop", Net {atoms = {...}, comb = ..., var = ...})}, comb = Leaf [], var = Leaf []}, var = Net {atoms = {}, comb = Net {atoms = {("HOL.Trueprop", ...)}, comb = Leaf [...], var = Leaf [...]}, var = Leaf []}}), ("Set.member", Net {atoms = {}, comb = Net {atoms = {}, comb = Net {atoms = {...}, comb = ..., var = ...}, var = Leaf []}, var = Leaf []}), ("HOL.implies", Net {atoms = {("HOL.True", Net {atoms = {}, comb = ..., var = ...}), ("HOL.False", Net {atoms = {}, ...})}, comb = Net {atoms = {}, comb = Net {atoms = {...}, ...}, var = Leaf [...]}, var = Net {atoms = {("HOL.True", ...), ...}, comb = Net {atoms = {...}, ...}, var = Leaf [...]}}), ("Groups.plus_class.plus", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {...}, comb = ..., var = ...}}), ("Groups.times_class.times", Net {atoms = {}, comb = Leaf [...], var = Net {atoms = {}, ...}}), ("Orderings.ord_class.less", Net {atoms = {...}, comb = ..., var = ...})}, comb = Net {atoms = {("HOL.If", Net {atoms = {("HOL.True", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Leaf [...], var = Leaf [...]}}), ("HOL.False", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = ..., var = ...}})}, comb = Net {atoms = {}, comb = Net {atoms = {("HOL.eq", Net {atoms = {}, ...})}, comb = Leaf [], var = Leaf []}, var = Leaf []}, var = Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Leaf [], var = Leaf [{elhs = ..., extra = false, ...}]}}}), ("Sum_Type.sum.case_sum", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Net {atoms = {...}, ...}, var = Leaf [...]}}}), ("Basic_BNF_LFPs.prod.size_prod", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = ..., var = ...}}})}, comb = Leaf [], var = Leaf []}, var = Leaf []}, var = Leaf []}, var = Leaf []}}, {congs = ({(?, "\?P \ ?P'; ?P' \ ?Q \ ?Q'\ \ ?P \ ?Q \ ?P' \ ?Q'"), (?, "\PROP ?P \ PROP ?P'; PROP ?P' \ PROP ?Q \ PROP ?Q'\ \ (PROP ?P =simp=> PROP ?Q) \ (PROP ?P' =simp=> PROP ?Q')")}, []), loop_tacs = [("split HOL.If :: (HOL.bool, (_, (_, _)fun)fun)fun", fn)], mk_rews = {mk = fn, mk_cong = fn, mk_eq_True = fn, mk_sym = fn, reorient = fn}, procs = Net {atoms = {}, comb = Net {atoms = {("HOL.Ex", Net {atoms = {}, comb = Leaf [], var = Leaf [Proc {lhs = Const ("HOL.Ex", "(...) ... bool") $ Abs ("x", "?'a", Var ((...), "?'a \ bool") $ ...), name = "HOL.defined_Ex", proc = fn, stamp = Stamp 93432}]}), ("HOL.All", Net {atoms = {}, comb = Leaf [], var = Leaf [Proc {lhs = Const ("HOL.All", "... ... ...") $ Abs ("x", "...", ... $ ...), name = "HOL.defined_All", proc = fn, stamp = Stamp 93476}]}), ("Pure.all", Net {atoms = {}, comb = Leaf [], var = Leaf [Proc {lhs = Const ("Pure.all", "...") $ Abs ("x", "...", ...), name = "HOL.defined_all", proc = fn, stamp = Stamp 93520}]})}, comb = Net {atoms = {("HOL.eq", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Leaf [], var = Leaf [Proc {lhs = Const ("...", ...) $ Var ((...), "?'a") $ ..., name = "HOL.neq", proc = fn, stamp = Stamp 93626}]}}), ("HOL.Let", Net {atoms = {}, comb = Leaf [], var = Net {atoms = {}, comb = Leaf [], var = Leaf [Proc {lhs = Const ("...", "?'a \ (?'a \ ?'b) \ ?'b") $ ... $ ..., name = "HOL.let_simp", proc = fn, stamp = Stamp 93750}]}}), ("Pure.imp", Net {atoms = {}, comb = Net {atoms = {("HOL.Trueprop", Net {atoms = {("HOL.False", ...)}, comb = Leaf [...], var = Leaf [...]})}, comb = Leaf [], var = Leaf []}, var = Leaf []}), ("Orderings.ord_class.less", Net {atoms = {}, comb = Net {atoms = {("Nat.Suc", Net {atoms = {}, comb = ..., var = ...})}, comb = Net {atoms = {("Groups.plus_class.plus", ...), ...}, comb = Leaf [...], var = Leaf [...]}, var = Leaf []}, var = Net {atoms = {}, comb = Net {atoms = {("Nat.Suc", ...)}, comb = Net {atoms = {...}, ...}, var = Leaf [...]}, var = Leaf []}})}, comb = Leaf [], var = Leaf []}, var = Leaf []}, var = Leaf []}, solvers = ([Solver {id = Stamp 93184, name = "HOL unsafe", solver = fn}], [Solver {id = Stamp 93186, name = "HOL safe", solver = fn}]), subgoal_tac = fn, term_ord = fn}): simpset val mk_finite = fn: term -> term val fresh_args = fn: Proof.context -> term -> term list val atom_ty = fn: typ -> typ val mk_atom_set = fn: term -> term val mk_fresh_star_ty = fn: typ -> term -> term -> term val fresh_star_ty = fn: typ -> typ val mk_full_horn = fn: (string * typ) list -> term list -> term -> term val atomize_rule = fn: Proof.context -> int -> thm -> thm val prove_termination_ind = fn: Proof.context -> int -> tactic val supp_const = fn: typ -> term val mk_diff = fn: term * term -> term val supp_rel_const = fn: typ -> term val setify_ty = fn: Proof.context -> typ -> term -> term val transform_prem2 = fn: Proof.context -> string list -> thm -> thm val fold_append = fn: term list -> term val atomize = fn: Proof.context -> thm -> thm val atom_const = fn: typ -> term val mk_supports = fn: term -> term -> term val fresh_star_const = fn: typ -> term val is_atom_list = fn: Proof.context -> typ -> bool val strip_full_horn = fn: term -> (string * typ) list * term list * term val fold_conj = fn: term list -> term val listify = fn: Proof.context -> term -> term val fold_union = fn: term list -> term val mk_union = fn: term * term -> term val mk_atom = fn: term -> term val mk_append = fn: term * term -> term val all_dtyp_constrs_types = fn: Old_Datatype_Aux.descr -> cns_info list val fold_union_env = fn: typ list -> term list -> term val mk_fresh = fn: term -> term -> term val is_atom_set = fn: Proof.context -> typ -> bool val mk_sort_of = fn: term -> term val listify_ty = fn: Proof.context -> typ -> term -> term val mk_atom_fset_ty = fn: typ -> term -> term val mk_fresh_star = fn: term -> term -> term val to_set_ty = fn: typ -> term -> term val mk_atom_ty = fn: typ -> term -> term val mk_supp_rel_ty = fn: typ -> term -> term -> term val prove_termination_fun = fn: thm list -> Proof.context -> Function.info * local_theory val atomify = fn: Proof.context -> term -> term val mk_atom_set_ty = fn: typ -> term -> term val atomify_ty = fn: Proof.context -> typ -> term -> term val supp_rel_ty = fn: typ -> typ val pat_completeness_simp = fn: thm list -> Proof.context -> tactic val mk_conj = fn: term * term -> term val finite_const = fn: typ -> term val setify = fn: Proof.context -> term -> term val is_atom = fn: Proof.context -> typ -> bool val mk_atom_fset = fn: term -> term val mk_atom_list_ty = fn: typ -> term -> term val transform_prem1 = fn: Proof.context -> string list -> thm -> thm val mk_finite_ty = fn: typ -> term -> term val mk_fresh_ty = fn: typ -> term -> term -> term val mk_binop_env = fn: typ list -> string -> term * term -> term val atomize_concl = fn: Proof.context -> thm -> thm val fresh_const = fn: typ -> term val fresh_ty = fn: typ -> typ val fold_conj_balanced = fn: term list -> term val supports_const = fn: typ -> term val to_set = fn: term -> term val mk_supp = fn: term -> term val mk_supports_ty = fn: typ -> term -> term -> term val supp_ty = fn: typ -> typ val mk_supp_rel = fn: term -> term -> term val mk_atom_list = fn: term -> term val mk_supp_ty = fn: typ -> term -> term ### ML warning (line 29 of "$AFP/Nominal2/nominal_atoms.ML"): ### Value identifier (arg) has not been referenced. signature ATOM_DECL = sig val add_atom_decl: binding * binding option -> theory -> theory end structure Atom_Decl: ATOM_DECL ### ML warning (line 40 of "$AFP/Nominal2/nominal_eqvt.ML"): ### Value identifier (context) has not been referenced. ### ML warning (line 77 of "$AFP/Nominal2/nominal_eqvt.ML"): ### Matches are not exhaustive. ### ML warning (line 93 of "$AFP/Nominal2/nominal_eqvt.ML"): ### Pattern is not exhaustive. ### ML warning (line 125 of "$AFP/Nominal2/nominal_eqvt.ML"): ### Pattern is not exhaustive. signature NOMINAL_EQVT = sig val equivariance_cmd: string -> Proof.context -> local_theory val raw_equivariance: Proof.context -> term list -> thm -> thm list -> thm list end structure Nominal_Eqvt: NOMINAL_EQVT ### theory "Nominal2.Nominal2_Base" ### 5.153s elapsed time, 19.544s cpu time, 1.264s GC time Loading theory "Nominal2.Nominal2_Abs" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2") ### Rewrite rule not in simpset: ### Wellfounded.accp alpha_set_rel ((?bs1, ?x1), ?R1, ?f1, ?p1, ?cs1, ?y1) \ ### alpha_set (?bs1, ?x1) ?R1 ?f1 ?p1 (?cs1, ?y1) \ ### ?f1 ?x1 - ?bs1 = ?f1 ?y1 - ?cs1 \ ### (?f1 ?x1 - ?bs1) \* ?p1 \ ?R1 (?p1 \ ?x1) ?y1 \ ?p1 \ ?bs1 = ?cs1 Found termination order: "{}" ### Rewrite rule not in simpset: ### Wellfounded.accp alpha_res_rel ((?bs1, ?x1), ?R1, ?f1, ?p1, ?cs1, ?y1) \ ### alpha_res (?bs1, ?x1) ?R1 ?f1 ?p1 (?cs1, ?y1) \ ### ?f1 ?x1 - ?bs1 = ?f1 ?y1 - ?cs1 \ ### (?f1 ?x1 - ?bs1) \* ?p1 \ ?R1 (?p1 \ ?x1) ?y1 Found termination order: "{}" ### Rewrite rule not in simpset: ### Wellfounded.accp alpha_lst_rel ((?bs1, ?x1), ?R1, ?f1, ?p1, ?cs1, ?y1) \ ### alpha_lst (?bs1, ?x1) ?R1 ?f1 ?p1 (?cs1, ?y1) \ ### ?f1 ?x1 - set ?bs1 = ?f1 ?y1 - set ?cs1 \ ### (?f1 ?x1 - set ?bs1) \* ?p1 \ ?R1 (?p1 \ ?x1) ?y1 \ ?p1 \ ?bs1 = ?cs1 Found termination order: "{}" ### Rewrite rule not in simpset: ### Wellfounded.accp alpha_abs_set_rel ((?bs1, ?x1), ?cs1, ?y1) \ ### alpha_abs_set (?bs1, ?x1) (?cs1, ?y1) \ ### \p. (?bs1, ?x1) \set (=) supp p (?cs1, ?y1) Found termination order: "{}" ### Rewrite rule not in simpset: ### Wellfounded.accp alpha_abs_lst_rel ((?bs1, ?x1), ?cs1, ?y1) \ ### alpha_abs_lst (?bs1, ?x1) (?cs1, ?y1) \ ### \p. (?bs1, ?x1) \lst (=) supp p (?cs1, ?y1) Found termination order: "{}" ### Rewrite rule not in simpset: ### Wellfounded.accp alpha_abs_res_rel ((?bs1, ?x1), ?cs1, ?y1) \ ### alpha_abs_res (?bs1, ?x1) (?cs1, ?y1) \ ### \p. (?bs1, ?x1) \res (=) supp p (?cs1, ?y1) Found termination order: "{}" ### 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__" ### ML warning (line 927 of "$AFP/Nominal2/Nominal2_Abs.thy"): ### Pattern is not exhaustive. val alpha_single_simproc = fn: thm -> 'a -> Proof.context -> cterm -> thm option Found termination order: "{}" ### theory "Nominal2.Nominal2_Abs" ### 2.546s elapsed time, 9.020s cpu time, 0.360s GC time Loading theory "Nominal2.Nominal2_FCB" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic" via "Nominal2.Nominal2") val all_trivials = fn: (Proof.context -> Proof.method) context_parser ### theory "Nominal2.Nominal2_FCB" ### 0.178s elapsed time, 0.720s cpu time, 0.000s GC time Loading theory "Nominal2.Nominal2" (required by "Robinson_Arithmetic.Instance" via "Robinson_Arithmetic.Robinson_Arithmetic") signature NOMINAL_DT_DATA = sig datatype alpha_result = AlphaResult of {alpha_bn_names: string list, alpha_bn_trms: term list, alpha_bn_tys: typ list, alpha_cases: thm list, alpha_intros: thm list, alpha_names: string list, alpha_raw_induct: thm, alpha_trms: term list, alpha_tys: typ list} datatype bclause = BC of bmode * (term option * int) list * int list datatype bmode = Lst | Res | Set type bn_info = term * int * (int * term option) list list val get_all_info: Proof.context -> (string * info) list val get_info: Proof.context -> string -> info option type info = {distinct: thm list, inject: thm list, strong_exhaust: thm list, strong_inducts: thm list} val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list datatype raw_dt_info = RawDtInfo of {raw_all_cns: term list list, raw_cns_info: cns_info list, raw_distinct_thms: thm list, raw_dt_names: string list, raw_dts: Old_Datatype.spec list, raw_exhaust_thms: thm list, raw_fp_sugars: BNF_FP_Def_Sugar.fp_sugar list, raw_induct_thm: thm, raw_induct_thms: thm list, raw_inject_thms: thm list, raw_size_thms: thm list, raw_size_trms: term list, raw_ty_args: (string * sort) list, raw_tys: typ list} val register_info: string * info -> Context.generic -> Context.generic val the_info: Proof.context -> string -> info datatype user_data = UserData of {bclauses: bclause list list list, bn_eqs: (Attrib.binding * term) list, bn_funs: (binding * typ * mixfix) list, cn_names: string list, cn_tys: (string * string) list, dts: Old_Datatype.spec list} end structure Nominal_Dt_Data: NOMINAL_DT_DATA type bn_info = term * int * (int * term option) list list datatype raw_dt_info = RawDtInfo of {raw_all_cns: term list list, raw_cns_info: cns_info list, raw_distinct_thms: thm list, raw_dt_names: string list, raw_dts: Old_Datatype.spec list, raw_exhaust_thms: thm list, raw_fp_sugars: BNF_FP_Def_Sugar.fp_sugar list, raw_induct_thm: thm, raw_induct_thms: thm list, raw_inject_thms: thm list, raw_size_thms: thm list, raw_size_trms: term list, raw_ty_args: (string * sort) list, raw_tys: typ list} datatype user_data = UserData of {bclauses: Nominal_Dt_Data.bclause list list list, bn_eqs: (Attrib.binding * term) list, bn_funs: (binding * typ * mixfix) list, cn_names: string list, cn_tys: (string * string) list, dts: Old_Datatype.spec list} datatype bmode = Lst | Res | Set datatype bclause = BC of bmode * (term option * int) list * int list type info = {distinct: thm list, inject: thm list, strong_exhaust: thm list, strong_inducts: thm list} datatype alpha_result = AlphaResult of {alpha_bn_names: string list, alpha_bn_trms: term list, alpha_bn_tys: typ list, alpha_cases: thm list, alpha_intros: thm list, alpha_names: string list, alpha_raw_induct: thm, alpha_trms: term list, alpha_tys: typ list} constructor Lst: bmode constructor UserData: {bclauses: bclause list list list, bn_eqs: (Attrib.binding * term) list, bn_funs: (binding * typ * mixfix) list, cn_names: string list, cn_tys: (string * string) list, dts: Old_Datatype.spec list} -> user_data val the_info = fn: Proof.context -> string -> info val register_info = fn: string * info -> Context.generic -> Context.generic val get_all_info = fn: Proof.context -> (string * info) list constructor BC: bmode * (term option * int) list * int list -> bclause val get_info = fn: Proof.context -> string -> info option constructor Res: bmode constructor AlphaResult: {alpha_bn_names: string list, alpha_bn_trms: term list, alpha_bn_tys: typ list, alpha_cases: thm list, alpha_intros: thm list, alpha_names: string list, alpha_raw_induct: thm, alpha_trms: term list, alpha_tys: typ list} -> alpha_result constructor RawDtInfo: {raw_all_cns: term list list, raw_cns_info: cns_info list, raw_distinct_thms: thm list, raw_dt_names: string list, raw_dts: Old_Datatype.spec list, raw_exhaust_thms: thm list, raw_fp_sugars: BNF_FP_Def_Sugar.fp_sugar list, raw_induct_thm: thm, raw_induct_thms: thm list, raw_inject_thms: thm list, raw_size_thms: thm list, raw_size_trms: term list, raw_ty_args: (string * sort) list, raw_tys: typ list} -> raw_dt_info constructor Set: bmode val mk_infos = fn: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list ### ML warning (line 82 of "$AFP/Nominal2/nominal_dt_rawfuns.ML"): ### Pattern is not exhaustive. ### ML warning (line 286 of "$AFP/Nominal2/nominal_dt_rawfuns.ML"): ### Value identifier (lthy) has not been referenced. ### ML warning (line 523 of "$AFP/Nominal2/nominal_dt_rawfuns.ML"): ### Pattern is not exhaustive. signature NOMINAL_DT_RAWFUNS = sig val define_raw_bn_perms: raw_dt_info -> bn_info list -> local_theory -> term list * thm list * local_theory val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> Specification.multi_specs -> local_theory -> term list * thm list * bn_info list * thm list * local_theory val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> Proof.context -> term list * term list * thm list * thm list * local_theory val define_raw_perms: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory val get_all_binders: bclause list -> (term option * int) list val is_recursive_binder: bclause -> bool val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list end structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS val get_all_binders = fn: bclause list -> (term option * int) list val raw_prove_eqvt = fn: term list -> thm list -> thm list -> Proof.context -> thm list val define_raw_bns = fn: raw_dt_info -> (binding * typ option * mixfix) list -> Specification.multi_specs -> local_theory -> term list * thm list * bn_info list * thm list * local_theory val define_raw_fvs = fn: raw_dt_info -> bn_info list -> bclause list list list -> Proof.context -> term list * term list * thm list * thm list * local_theory val define_raw_bn_perms = fn: raw_dt_info -> bn_info list -> local_theory -> term list * thm list * local_theory val is_recursive_binder = fn: bclause -> bool val define_raw_perms = fn: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory ### Metis: Unused theorems: "Nominal2_Base.pt_class.permute_minus_cancel_2" ### Metis: Unused theorems: "Set.empty_subsetI", "local.insert_3", "Nominal2_Base.supp_swap" ### Ignoring duplicate rewrite rule: ### ?a1 \ atom ?b1 \ ?a1 \ ?b1 ### ML warning (line 385 of "$AFP/Nominal2/nominal_dt_alpha.ML"): ### Pattern is not exhaustive. ### ML warning (line 604 of "$AFP/Nominal2/nominal_dt_alpha.ML"): ### Value identifier (alpha_bn_names) has not been referenced. ### ML warning (line 604 of "$AFP/Nominal2/nominal_dt_alpha.ML"): ### Value identifier (alpha_names) has not been referenced. ### ML warning (line 828 of "$AFP/Nominal2/nominal_dt_alpha.ML"): ### Pattern is not exhaustive. signature NOMINAL_DT_ALPHA = sig val alpha_prove: term list -> (term * (term * term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val mk_alpha_permute_rsp: Proof.context -> thm -> thm val mk_funs_rsp: Proof.context -> thm -> thm val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA val raw_size_rsp_aux = fn: Proof.context -> alpha_result -> thm list -> thm list val induct_prove = fn: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_prove_refl = fn: Proof.context -> alpha_result -> thm -> thm list val raw_prove_trans = fn: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_fv_bn_rsp_aux = fn: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_perm_bn_rsp = fn: Proof.context -> alpha_result -> term list -> thm list -> thm list val alpha_prove = fn: term list -> (term * (term * term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_alpha_bn_rsp = fn: alpha_result -> thm list -> thm list -> thm list val define_raw_alpha = fn: raw_dt_info -> bn_info list -> bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val raw_prove_alpha_distincts = fn: Proof.context -> alpha_result -> raw_dt_info -> thm list val comb_binders = fn: Proof.context -> bmode -> term list -> (term option * int) list -> term val raw_prove_equivp = fn: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list val raw_constrs_rsp = fn: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_prove_alpha_eq_iff = fn: Proof.context -> alpha_result -> raw_dt_info -> thm list val mk_alpha_permute_rsp = fn: Proof.context -> thm -> thm val mk_funs_rsp = fn: Proof.context -> thm -> thm val raw_prove_bn_imp = fn: Proof.context -> alpha_result -> thm list val raw_prove_sym = fn: Proof.context -> alpha_result -> thm list -> thm list ### ML warning (line 80 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Value identifier (lhs_ty) has not been referenced. ### ML warning (line 80 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Value identifier (lhs_str) has not been referenced. ### ML warning (line 248 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Value identifier (qtys) has not been referenced. ### ML warning (line 292 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Value identifier (ctxt) has not been referenced. ### ML warning (line 368 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Pattern is not exhaustive. ### ML warning (line 389 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Pattern is not exhaustive. ### ML warning (line 571 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Pattern is not exhaustive. ### ML warning (line 623 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Pattern is not exhaustive. ### ML warning (line 666 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Value identifier (c) has not been referenced. ### ML warning (line 705 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Pattern is not exhaustive. ### ML warning (line 707 of "$AFP/Nominal2/nominal_dt_quot.ML"): ### Pattern is not exhaustive. signature NOMINAL_DT_QUOT = sig val define_qconsts: typ list -> (string * term * mixfix * thm) list -> local_theory -> Quotient_Info.quotconsts list * local_theory val define_qperms: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory val define_qsizes: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> local_theory -> local_theory val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> thm list -> local_theory -> Quotient_Info.quotients list * local_theory val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> thm list val prove_supports: Proof.context -> thm list -> term list -> thm list end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT val prove_permute_bn_thms = fn: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val define_qsizes = fn: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> local_theory -> local_theory val prove_strong_exhausts = fn: Proof.context -> thm list -> bclause list list list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list val prove_bns_finite = fn: typ list -> term list -> thm -> thm list -> Proof.context -> thm list val prove_fsupp = fn: Proof.context -> typ list -> thm -> thm list -> thm list val prove_fv_supp = fn: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list val prove_supports = fn: Proof.context -> thm list -> term list -> thm list val prove_perm_bn_alpha_thms = fn: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val define_qtypes = fn: (string list * binding * mixfix) list -> typ list -> term list -> thm list -> local_theory -> Quotient_Info.quotients list * local_theory val lift_thms = fn: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context val define_qperms = fn: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory val prove_strong_induct = fn: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> thm list val fs_instance = fn: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory val define_qconsts = fn: typ list -> (string * term * mixfix * thm) list -> local_theory -> Quotient_Info.quotconsts list * local_theory ### ML warning (line 17 of "$AFP/Nominal2/nominal_induct.ML"): ### Value identifier (tupleT) has not been referenced. ### ML warning (line 50 of "$AFP/Nominal2/nominal_induct.ML"): ### Pattern is not exhaustive. structure NominalInduct: sig val nominal_induct_method: (Proof.context -> Proof.method) context_parser val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list -> (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> context_tactic end ### Ignoring duplicate rewrite rule: ### (?p1 + ?q1) \ ?x1 \ ?p1 \ ?q1 \ ?x1 ### Metis: Unused theorems: "Nominal2_Base.eqvt_apply" ### ML warning (line 137 of "$AFP/Nominal2/nominal_inductive.ML"): ### Matches are not exhaustive. ### ML warning (line 247 of "$AFP/Nominal2/nominal_inductive.ML"): ### Pattern is not exhaustive. ### ML warning (line 312 of "$AFP/Nominal2/nominal_inductive.ML"): ### Pattern is not exhaustive. ### ML warning (line 342 of "$AFP/Nominal2/nominal_inductive.ML"): ### Pattern is not exhaustive. signature NOMINAL_INDUCTIVE = sig val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list -> Proof.context -> Proof.state val prove_strong_inductive_cmd: xstring * (string * string list) list -> Proof.context -> Proof.state end structure Nominal_Inductive: NOMINAL_INDUCTIVE ### ML warning (line 101 of "$AFP/Nominal2/nominal_function_common.ML"): ### Value identifier (data) has not been referenced. ### ML warning (line 103 of "$AFP/Nominal2/nominal_function_common.ML"): ### Pattern is not exhaustive. ### ML warning (line 144 of "$AFP/Nominal2/nominal_function_common.ML"): ### Value identifier (inv) has not been referenced. ### ML warning (line 141 of "$AFP/Nominal2/nominal_function_common.ML"): ### Value identifier (partials) has not been referenced. ### ML warning (line 138 of "$AFP/Nominal2/nominal_function_common.ML"): ### Value identifier (domintros) has not been referenced. ### ML warning (line 135 of "$AFP/Nominal2/nominal_function_common.ML"): ### Value identifier (default) has not been referenced. ### ML warning (line 132 of "$AFP/Nominal2/nominal_function_common.ML"): ### Value identifier (sequential) has not been referenced. signature NOMINAL_FUNCTION_DATA = sig type nominal_info = {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: string, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} end structure Nominal_Function_Common: sig structure NominalFunctionData: GENERIC_DATA val add_function_data: nominal_info -> Context.generic -> Context.generic val all_function_data: Proof.context -> (term * nominal_info) list val apply_opt: nominal_function_opt -> nominal_function_config -> nominal_function_config val get_function: Proof.context -> NominalFunctionData.T val import_function_data: term -> Proof.context -> {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: bstring, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} option val import_last_function: Proof.context -> {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: bstring, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} option val lift_morphism: Proof.context -> (thm -> thm) -> morphism val morph_function_data: nominal_info -> morphism -> {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: bstring, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} val nominal_default_config: nominal_function_config datatype nominal_function_config = NominalFunctionConfig of {default: string option, domintros: bool, inv: string option, partials: bool, sequential: bool} datatype nominal_function_opt = Default of string | DomIntros | Invariant of string | No_Partials | Sequential datatype nominal_function_result = NominalFunctionResult of {G: term, R: term, cases: thm, domintros: thm list option, eqvts: thm list, fs: term list, psimps: thm list, simple_pinducts: thm list, termination: thm} type nominal_info = {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: string, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} end ### Ignoring duplicate rewrite rule: ### ?P1 \ ?Q1 \ ?P1 \ ?Q1 ### ML warning (line 100 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (case_split) has not been referenced. ### ML warning (line 101 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (fundef_default_value) has not been referenced. ### ML warning (line 102 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (not_acc_down) has not been referenced. ### ML warning (line 279 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (thms) has not been referenced. ### ML warning (line 296 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (case_hypi) has not been referenced. ### ML warning (line 297 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (case_hypj) has not been referenced. ### ML warning (line 336 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (lhs) has not been referenced. ### ML warning (line 603 of "$AFP/Nominal2/nominal_function_core.ML"): ### Pattern is not exhaustive. ### ML warning (line 603 of "$AFP/Nominal2/nominal_function_core.ML"): ### Value identifier (raw_induct) has not been referenced. ### ML warning (line 631 of "$AFP/Nominal2/nominal_function_core.ML"): ### Matches are not exhaustive. ### ML warning (line 699 of "$AFP/Nominal2/nominal_function_core.ML"): ### Pattern is not exhaustive. ### ML warning (line 997 of "$AFP/Nominal2/nominal_function_core.ML"): ### Matches are not exhaustive. signature NOMINAL_FUNCTION_CORE = sig val inductive_def: (binding * typ) * mixfix -> term list -> local_theory -> (term * thm list * thm * thm) * local_theory val prepare_nominal_function: Nominal_Function_Common.nominal_function_config -> string -> ((bstring * typ) * mixfix) list -> ((bstring * typ) list * term list * term * term) list -> local_theory -> (term * term * thm list * thm * thm * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result)) * local_theory val trace: bool ref end structure Nominal_Function_Core: NOMINAL_FUNCTION_CORE ### ML warning (line 100 of "$AFP/Nominal2/nominal_mutual.ML"): ### Pattern is not exhaustive. ### ML warning (line 183 of "$AFP/Nominal2/nominal_mutual.ML"): ### Pattern is not exhaustive. ### ML warning (line 209 of "$AFP/Nominal2/nominal_mutual.ML"): ### Pattern is not exhaustive. ### ML warning (line 220 of "$AFP/Nominal2/nominal_mutual.ML"): ### Pattern is not exhaustive. ### ML warning (line 307 of "$AFP/Nominal2/nominal_mutual.ML"): ### Value identifier (insts) has not been referenced. ### ML warning (line 309 of "$AFP/Nominal2/nominal_mutual.ML"): ### Pattern is not exhaustive. ### ML warning (line 359 of "$AFP/Nominal2/nominal_mutual.ML"): ### Pattern is not exhaustive. ### ML warning (line 363 of "$AFP/Nominal2/nominal_mutual.ML"): ### Matches are not exhaustive. ### ML warning (line 369 of "$AFP/Nominal2/nominal_mutual.ML"): ### Matches are not exhaustive. ### ML warning (line 372 of "$AFP/Nominal2/nominal_mutual.ML"): ### Value identifier (f) has not been referenced. ### ML warning (line 372 of "$AFP/Nominal2/nominal_mutual.ML"): ### Matches are not exhaustive. ### ML warning (line 395 of "$AFP/Nominal2/nominal_mutual.ML"): ### Value identifier (Q) has not been referenced. ### ML warning (line 395 of "$AFP/Nominal2/nominal_mutual.ML"): ### Matches are not exhaustive. ### ML warning (line 423 of "$AFP/Nominal2/nominal_mutual.ML"): ### Value identifier (fvar) has not been referenced. signature NOMINAL_FUNCTION_MUTUAL = sig val prepare_nominal_function_mutual: Nominal_Function_Common.nominal_function_config -> string -> ((string * typ) * mixfix) list -> term list -> local_theory -> (thm * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result)) * local_theory end structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL ### ML warning (line 60 of "$AFP/Nominal2/nominal_function.ML"): ### Value identifier (rvs) has not been referenced. ### ML warning (line 158 of "$AFP/Nominal2/nominal_function.ML"): ### Pattern is not exhaustive. ### ML warning (line 145 of "$AFP/Nominal2/nominal_function.ML"): ### Matches are not exhaustive. signature NOMINAL_FUNCTION = sig val add_nominal_function: (binding * typ option * mixfix) list -> Specification.multi_specs -> Nominal_Function_Common.nominal_function_config -> (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory val add_nominal_function_cmd: (binding * string option * mixfix) list -> Specification.multi_specs_cmd -> Nominal_Function_Common.nominal_function_config -> (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory val get_info: Proof.context -> term -> nominal_info val nominal_function: (binding * typ option * mixfix) list -> Specification.multi_specs -> Nominal_Function_Common.nominal_function_config -> local_theory -> Proof.state val nominal_function_cmd: (binding * string option * mixfix) list -> Specification.multi_specs_cmd -> Nominal_Function_Common.nominal_function_config -> bool -> local_theory -> Proof.state type nominal_info = {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: string, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} end structure Nominal_Function: NOMINAL_FUNCTION ### ML warning (line 67 of "$AFP/Nominal2/nominal_termination.ML"): ### Value identifier (eqvts) has not been referenced. ### ML warning (line 47 of "$AFP/Nominal2/nominal_termination.ML"): ### Matches are not exhaustive. signature NOMINAL_FUNCTION_TERMINATION = sig type nominal_info = {R: term, add_simps: (binding -> binding) -> string -> (binding -> binding) -> Token.src list -> thm list -> local_theory -> thm list * local_theory , case_names: string list, defname: string, eqvts: thm list, fs: term list, inducts: thm list option, is_partial: bool, pinducts: thm list, psimps: thm list, simps: thm list option, termination: thm} val termination: bool -> term option -> local_theory -> Proof.state val termination_cmd: bool -> string option -> local_theory -> Proof.state end structure Nominal_Function_Termination: NOMINAL_FUNCTION_TERMINATION val eqvt_attr = [Token (("attribute", ({}, {})), (String, "attribute"), Value ( SOME ( Name ({kind = "attribute", name = "Pure.attribute", print = fn}, {}) ) )), Token (("", ({}, {})), (String, ""), Value (SOME (Attribute fn)))]: Token.src val simp_attr = [Token (("attribute", ({}, {})), (String, "attribute"), Value ( SOME ( Name ({kind = "attribute", name = "Pure.attribute", print = fn}, {}) ) )), Token (("", ({}, {})), (String, ""), Value (SOME (Attribute fn)))]: Token.src val induct_attr = [Token (("attribute", ({}, {})), (String, "attribute"), Value ( SOME ( Name ({kind = "attribute", name = "Pure.attribute", print = fn}, {}) ) )), Token (("", ({}, {})), (String, ""), Value (SOME (Attribute fn)))]: Token.src val get_cnstrs = fn: ('a * 'b) list -> 'b list val get_typed_cnstrs = fn: ((binding * 'a * 'b) * (binding * 'c * 'd) list) list -> (bstring * bstring) list val get_cnstr_strs = fn: ('a * (binding * 'b * 'c) list) list -> bstring list val get_bn_fun_strs = fn: (binding * 'a * 'b) list -> bstring list ### ML warning (line 80 of "$AFP/Nominal2/Nominal2.thy"): ### Value identifier (ty_ss) has not been referenced. ### ML warning (line 95 of "$AFP/Nominal2/Nominal2.thy"): ### Value identifier (trm_ss) has not been referenced. val add_raw = fn: string -> string val add_raws = fn: string list -> string list val raw_bind = fn: binding -> binding val replace_str = fn: (''a * ''a) list -> ''a -> ''a val replace_typ = fn: (string * string) list -> typ -> typ val raw_dts = fn: (string * string) list -> ((binding * 'a * 'b) * (binding * typ list * 'c) list) list -> ((binding * 'a * mixfix) * (binding * typ list * mixfix) list) list val replace_aterm = fn: (string * string) list -> term -> term val replace_term = fn: (string * string) list -> (string * string) list -> term -> term val rawify_dts = fn: ((binding * 'a * 'b) * (binding * typ list * 'c) list) list -> (string * string) list -> ((binding * 'a * mixfix) * (binding * typ list * mixfix) list) list val rawify_bn_funs = fn: (string * string) list -> (string * string) list -> (string * string) list -> (binding * typ * 'a) list -> ('b * term) list -> (binding * typ option * mixfix) list * (('b * term) * 'c list * 'd list) list val rawify_bclauses = fn: (string * string) list -> (string * string) list -> (string * string) list -> bclause list list list -> bclause list list list val define_raw_dts = fn: ((binding * (string * sort) list * 'a) * (binding * typ list * 'b) list) list -> string list -> (string * string) list -> (binding * typ * 'c) list -> ('d * term) list -> bclause list list list -> local_theory -> bclause list list list * (binding * typ option * mixfix) list * (('d * term) * 'e list * 'f list) list * raw_dt_info * local_theory Found termination order: "{}" ### ML warning (line 229 of "$AFP/Nominal2/Nominal2.thy"): ### Value identifier (raw_induct_thms) has not been referenced. ### ML warning (line 224 of "$AFP/Nominal2/Nominal2.thy"): ### Value identifier (raw_fp_sugars) has not been referenced. ### ML warning (line 222 of "$AFP/Nominal2/Nominal2.thy"): ### Value identifier (raw_tys) has not been referenced. ### ML warning (line 221 of "$AFP/Nominal2/Nominal2.thy"): ### Value identifier (raw_dt_names) has not been referenced. ### ML warning (line 412 of "$AFP/Nominal2/Nominal2.thy"): ### Pattern is not exhaustive. val nominal_datatype2 = fn: binding option -> ((binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list ) list -> (binding * typ * mixfix) list -> (Attrib.binding * term) list -> bclause list list list -> local_theory -> local_theory val augment_sort = fn: theory -> sort -> sort val augment_sort_typ = fn: theory -> typ -> typ val prepare_dts = fn: ((binding * (string * string option) list * mixfix) * (binding * ('a * string) list * mixfix * 'b) list ) list -> theory -> ((binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list ) list * theory val prepare_bn_funs = fn: (binding * string option * mixfix) list -> Specification.multi_specs_cmd -> theory -> ((binding * typ * mixfix) list * (Attrib.binding * term) list) * theory ### ML warning (line 618 of "$AFP/Nominal2/Nominal2.thy"): ### (=) has infix status but was not preceded by op. val indexify = fn: 'a option list -> ('a * int) list val index_lookup = fn: (string * 'a) list -> string -> 'a val prepare_bclauses = fn: ('a * ('b * (string option * 'c) list * 'd * (bmode * string list * string list) list ) list ) list -> theory -> bclause list list list * theory ### ML warning (line 666 of "$AFP/Nominal2/Nominal2.thy"): ### (=) has infix status but was not preceded by op. val included = fn: int -> bclause list -> bool val complete = fn: ('a * ('b * 'c list * 'd * 'e) list) list -> bclause list list list -> bclause list list list val nominal_datatype2_cmd = fn: binding option * ((binding * (string * string option) list * mixfix) * (binding * (string option * string) list * mixfix * (bmode * string list * string list) list ) list ) list * (binding * string option * mixfix) list * Specification.multi_specs_cmd -> Proof.context -> local_theory val opt_name = fn: Token.T list -> binding option * Token.T list val anno_typ = fn: Token.T list -> (string option * string) * Token.T list val bind_mode = fn: Token.T list -> bmode * Token.T list val bind_clauses = fn: (bmode * string list * string list) list parser val cnstr_parser = fn: Token.T list -> (binding * (string option * string) list * mixfix * (bmode * string list * string list) list) * Token.T list val dt_parser = fn: Token.T list -> ((binding * (string * string option) list * mixfix) * (binding * (string option * string) list * mixfix * (bmode * string list * string list) list ) list) * Token.T list val bnfun_parser = fn: Token.T list -> ((binding * string option * mixfix) list * Specification.multi_specs_cmd) * Token.T list val main_parser = fn: Token.T list -> (binding option * ((binding * (string * string option) list * mixfix) * (binding * (string option * string) list * mixfix * (bmode * string list * string list) list ) list ) list * (binding * string option * mixfix) list * Specification.multi_specs_cmd) * Token.T list ### theory "Nominal2.Nominal2" ### 3.469s elapsed time, 13.200s cpu time, 0.356s GC time Loading theory "Robinson_Arithmetic.Robinson_Arithmetic" (required by "Robinson_Arithmetic.Instance") ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" Proofs for inductive predicate(s) "boolean_axiomsp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "special_axiomsp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "nprv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Robinson_Arithmetic.Robinson_Arithmetic" ### 7.091s elapsed time, 16.976s cpu time, 0.672s GC time Loading theory "Robinson_Arithmetic.Instance" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" *** Failed to apply proof method (line 167 of "$AFP/Robinson_Arithmetic/Robinson_Arithmetic.thy"): *** goal (3 subgoals): *** 1. \k e A ka Aa. *** \\x. \p. (p \ eval_fmla_sumC) *** (finfun_update (p \ e) (p \ k) x, p \ A) = *** eval_fmla_sumC (finfun_update (p \ e) (p \ k) x, p \ A); *** \x. \p. (p \ eval_fmla_sumC) *** (finfun_update (p \ e) (p \ ka) x, p \ Aa) = *** eval_fmla_sumC (finfun_update (p \ e) (p \ ka) x, p \ Aa); *** atom k \ e; atom ka \ e\ *** \ atom k \ ea \ atom ka \ ea *** 2. \k e A ka Aa p. *** \\x. \p. (p \ eval_fmla_sumC) *** (finfun_update (p \ e) (p \ k) x, p \ A) = *** eval_fmla_sumC (finfun_update (p \ e) (p \ k) x, p \ A); *** \x. \p. (p \ eval_fmla_sumC) *** (finfun_update (p \ e) (p \ ka) x, p \ Aa) = *** eval_fmla_sumC (finfun_update (p \ e) (p \ ka) x, p \ Aa); *** atom k \ e; atom ka \ e; supp p \* ea\ *** \ (\x. eval_fmla_sumC (finfun_update (p \ e) (p \ k) x, p \ A)) = *** (\x. eval_fmla_sumC (finfun_update e (p \ k) x, p \ A)) *** 3. \k e A ka Aa p. *** \\x. \p. (p \ eval_fmla_sumC) *** (finfun_update (p \ e) (p \ k) x, p \ A) = *** eval_fmla_sumC (finfun_update (p \ e) (p \ k) x, p \ A); *** \x. \p. (p \ eval_fmla_sumC) *** (finfun_update (p \ e) (p \ ka) x, p \ Aa) = *** eval_fmla_sumC (finfun_update (p \ e) (p \ ka) x, p \ Aa); *** atom k \ e; atom ka \ e; supp p \* ea\ *** \ (\x. eval_fmla_sumC (finfun_update (p \ e) (p \ ka) x, p \ Aa)) = *** (\x. eval_fmla_sumC (finfun_update e (p \ ka) x, p \ Aa)) Proofs for inductive predicate(s) "nump" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Robinson_Arithmetic.Instance" ### 1.513s elapsed time, 5.872s cpu time, 0.304s GC time *** Failed to apply proof method (line 167 of "$AFP/Robinson_Arithmetic/Robinson_Arithmetic.thy"): *** goal (3 subgoals): *** 1. ⋀k e A ka Aa. *** ⟦⋀x. ∀p. (p ∙ eval_fmla_sumC) *** (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A) = *** eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A); *** ⋀x. ∀p. (p ∙ eval_fmla_sumC) *** (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa) = *** eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa); *** atom k ♯ e; atom ka ♯ e⟧ *** ⟹ atom k ♯ ea ∧ atom ka ♯ ea *** 2. ⋀k e A ka Aa p. *** ⟦⋀x. ∀p. (p ∙ eval_fmla_sumC) *** (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A) = *** eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A); *** ⋀x. ∀p. (p ∙ eval_fmla_sumC) *** (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa) = *** eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa); *** atom k ♯ e; atom ka ♯ e; supp p ♯* ea⟧ *** ⟹ (∃x. eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A)) = *** (∃x. eval_fmla_sumC (finfun_update e (p ∙ k) x, p ∙ A)) *** 3. ⋀k e A ka Aa p. *** ⟦⋀x. ∀p. (p ∙ eval_fmla_sumC) *** (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A) = *** eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ k) x, p ∙ A); *** ⋀x. ∀p. (p ∙ eval_fmla_sumC) *** (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa) = *** eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa); *** atom k ♯ e; atom ka ♯ e; supp p ♯* ea⟧ *** ⟹ (∃x. eval_fmla_sumC (finfun_update (p ∙ e) (p ∙ ka) x, p ∙ Aa)) = *** (∃x. eval_fmla_sumC (finfun_update e (p ∙ ka) x, p ∙ Aa)) *** At command "apply" (line 167 of "$AFP/Robinson_Arithmetic/Robinson_Arithmetic.thy")