Loading theory "HOL-Library.AList" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Finite_Map") Loading theory "HOL-Library.Adhoc_Overloading" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Monad_Syntax") Loading theory "HOL-Library.Conditional_Parametricity" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Finite_Map") Loading theory "HOL-Library.Nat_Bijection" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Finite_Map" via "HOL-Library.FSet" via "HOL-Library.Countable") consts update :: "'key \ 'val \ ('key \ 'val) list \ ('key \ 'val) list" Found termination order: "(\p. size (snd p)) <*mlex*> {}" signature ADHOC_OVERLOADING = sig val generic_add_overloaded: string -> Context.generic -> Context.generic val generic_add_variant: string -> term -> Context.generic -> Context.generic val generic_remove_overloaded: string -> Context.generic -> Context.generic val generic_remove_variant: string -> term -> Context.generic -> Context.generic val is_overloaded: Proof.context -> string -> bool val show_variants: bool Config.T end structure Adhoc_Overloading: ADHOC_OVERLOADING ### theory "HOL-Library.Adhoc_Overloading" ### 0.181s elapsed time, 0.776s cpu time, 0.000s GC time Loading theory "HOL-Library.Monad_Syntax" (required by "Higher_Order_Terms.Term_Utils") ### theory "HOL-Library.Monad_Syntax" ### 0.051s elapsed time, 0.204s cpu time, 0.000s GC time Loading theory "HOL-Library.State_Monad" (required by "Higher_Order_Terms.Term_Utils") Found termination order: "size_list size <*mlex*> {}" consts update_with_aux :: "'val \ 'key \ ('val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" ### theory "HOL-Library.Nat_Bijection" ### 0.626s elapsed time, 2.520s cpu time, 0.000s GC time Loading theory "HOL-Library.Old_Datatype" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Finite_Map" via "HOL-Library.FSet" via "HOL-Library.Countable") signature CONDITIONAL_PARAMETRICITY = sig exception WARNING of string val default_settings: settings val get_parametricity_theorems: Proof.context -> thm list val mk_cond_goal: Proof.context -> thm -> term * thm val mk_goal: Proof.context -> term -> term val mk_param_goal_from_eq_def: Proof.context -> thm -> term val parametric_constant: settings -> Attrib.binding * thm -> Proof.context -> thm * Proof.context val prove_find_goal_cond: settings -> Proof.context -> thm list -> thm option -> term -> thm val prove_goal: settings -> Proof.context -> thm option -> term -> thm val quiet_settings: settings type settings = {suppress_print_theorem: bool, suppress_warnings: bool, use_equality_heuristic: bool, warnings_as_errors: bool} val step_tac: settings -> Proof.context -> thm list -> int -> tactic end structure Conditional_Parametricity: CONDITIONAL_PARAMETRICITY ### theory "HOL-Library.Conditional_Parametricity" ### 0.709s elapsed time, 2.860s cpu time, 0.000s GC time Loading theory "List-Index.List_Index" (required by "Higher_Order_Terms.Find_First") consts find_index :: "('a \ bool) \ 'a list \ nat" consts map_index' :: "nat \ (nat \ 'a \ 'b) \ 'a list \ 'b list" consts insert_nth :: "nat \ 'a \ 'a list \ 'a list" Found termination order: "(\p. length (snd p)) <*mlex*> {}" ### theory "List-Index.List_Index" ### 0.823s elapsed time, 3.256s cpu time, 0.344s GC time Found termination order: "(\p. length (snd p)) <*mlex*> {}" 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.949s elapsed time, 3.760s cpu time, 0.344s GC time Loading theory "HOL-Library.Countable" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Finite_Map" via "HOL-Library.FSet") ### theory "HOL-Library.State_Monad" ### 1.450s elapsed time, 5.744s cpu time, 0.344s GC time Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. size_list size (snd (snd (snd p)))) <*mlex*> {}" ### theory "HOL-Library.AList" ### 2.279s elapsed time, 8.968s cpu time, 0.344s GC time ### 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 ... ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g val old_countable_datatype_tac = fn: Proof.context -> int -> tactic ### ML warning (line 93 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 139 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. ### ML warning (line 143 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 145 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Matches are not exhaustive. ### ML warning (line 156 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"): ### Pattern is not exhaustive. signature BNF_LFP_COUNTABLE = sig val countable_datatype_tac: Proof.context -> tactic val derive_encode_injectives_thms: Proof.context -> string list -> thm list end structure BNF_LFP_Countable: BNF_LFP_COUNTABLE val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq val countable_tac = fn: Proof.context -> int -> tactic ### theory "HOL-Library.Countable" ### 2.002s elapsed time, 7.708s cpu time, 0.396s GC time Loading theory "HOL-Library.FSet" (required by "Higher_Order_Terms.Term_Utils" via "HOL-Library.Finite_Map") 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 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 ### Rule already declared as introduction (intro) ### (\a s s'. ### run_state ?m s = (a, s') \ ?P s s') \ ### state_io_rel ?P ?m ### Rule already declared as introduction (intro) ### (\a s s'. ### run_state ?m s = (a, s') \ ?P s s') \ ### state_io_rel ?P ?m ### Rule already declared as elimination (elim) ### \state_io_rel ?P ?m; run_state ?m ?s = (?a, ?s'); ### ?P ?s ?s' \ PROP ?W\ ### \ PROP ?W ### Rule already declared as elimination (elim) ### \state_io_rel ?P ?m; run_state ?m ?s = (?a, ?s'); ### ?P ?s ?s' \ PROP ?W\ ### \ PROP ?W ### Rule already declared as elimination (elim) ### \state_io_rel ?P ?m; run_state ?m ?s = (?a, ?s'); ### ?P ?s ?s' \ PROP ?W\ ### \ PROP ?W ### Rule already declared as introduction (intro) ### (\a s s'. ### run_state ?m s = (a, s') \ ?P s s') \ ### state_io_rel ?P ?m ### Rule already declared as introduction (intro) ### (\a s s'. ### run_state ?m s = (a, s') \ ?P s s') \ ### state_io_rel ?P ?m 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" ### 5.593s elapsed time, 21.224s cpu time, 0.684s GC time Loading theory "HOL-Library.Finite_Map" (required by "Higher_Order_Terms.Term_Utils") theorem map_add_transfer: rel_fun (rel_fun ?A1.0 (rel_option ?A2.0)) (rel_fun (rel_fun ?A1.0 (rel_option ?A2.0)) (rel_fun ?A1.0 (rel_option ?A2.0))) (++) (++) theorem map_of_transfer: bi_unique ?A1.0 \ rel_fun (list_all2 (rel_prod ?A1.0 ?A2.0)) (rel_fun ?A1.0 (rel_option ?A2.0)) map_of map_of ### Introduced fixed type variable(s): 'd in "m__" or "n__" theorem dom_transfer: bi_total ?A1.0 \ ((?A1.0 ===> rel_option ?A2.0) ===> rel_set ?A1.0) dom dom theorem map_upd_transfer: bi_unique ?A1.0 \ (?A1.0 ===> ?A2.0 ===> (?A1.0 ===> rel_option ?A2.0) ===> ?A1.0 ===> rel_option ?A2.0) map_upd map_upd theorem map_filter_transfer: ((?A1.0 ===> (=)) ===> (?A1.0 ===> rel_option ?A2.0) ===> ?A1.0 ===> rel_option ?A2.0) map_filter map_filter theorem map_drop_transfer: bi_unique ?A1.0 \ (?A1.0 ===> (?A1.0 ===> rel_option ?A2.0) ===> ?A1.0 ===> rel_option ?A2.0) map_drop map_drop theorem map_drop_set_transfer: bi_unique ?A1.0 \ (rel_set ?A1.0 ===> (?A1.0 ===> rel_option ?A2.0) ===> ?A1.0 ===> rel_option ?A2.0) map_drop_set map_drop_set theorem map_restrict_set_transfer: bi_unique ?A1.0 \ (rel_set ?A1.0 ===> (?A1.0 ===> rel_option ?A2.0) ===> ?A1.0 ===> rel_option ?A2.0) map_restrict_set map_restrict_set theorem map_pred_transfer: bi_total ?A1.0 \ ((?A1.0 ===> ?A2.0 ===> (=)) ===> (?A1.0 ===> rel_option ?A2.0) ===> (=)) map_pred map_pred ### Introduced fixed type variable(s): 'c, 'd in "x__" or "y__" theorem map_comp_transfer: ((?A3.0 ===> rel_option ?A2.0) ===> (?A1.0 ===> rel_option ?A3.0) ===> ?A1.0 ===> rel_option ?A2.0) (\\<^sub>m) (\\<^sub>m) instantiation fmap :: (type, type) size size_fmap == size :: ('a, 'b) fmap \ nat ### Metis: Unused theorems: "Hilbert_Choice.bchoice" ### Introduced fixed type variable(s): 'd in "m__" or "n__" ### Introduced fixed type variable(s): 'd in "m__" instantiation fmap :: (type, equal) equal equal_fmap == equal_class.equal :: ('a, 'b) fmap \ ('a, 'b) fmap \ bool ### Introduced fixed type variable(s): 'c, 'd in "ma__" datatype 'a ref = ref of 'a ROOT.ML:49: warning: Value identifier (p) has not been referenced. ROOT.ML:52: warning: Matches are not exhaustive. Found near fun ball (Set xs) p = list_all p xs ROOT.ML:54: warning: Value identifier (f) has not been referenced. ROOT.ML:57: warning: Matches are not exhaustive. Found near fun image f (... ...) = Set (... ... xs) ROOT.ML:63: warning: Value identifier (f) has not been referenced. ROOT.ML:67: warning: Value identifier (k) has not been referenced. ROOT.ML:67: warning: Value identifier (A_) has not been referenced. ROOT.ML:69: warning: Value identifier (y) has not been referenced. ROOT.ML:69: warning: Value identifier (A_) has not been referenced. ROOT.ML:75: warning: Value identifier (x2) has not been referenced. ROOT.ML:77: warning: Value identifier (A_) has not been referenced. ROOT.ML:85: warning: Value identifier (p) has not been referenced. ROOT.ML:92: warning: Value identifier (x1) has not been referenced. ROOT.ML:94: warning: Value identifier (ys) has not been referenced. ROOT.ML:94: warning: Value identifier (B_) has not been referenced. ROOT.ML:94: warning: Value identifier (A_) has not been referenced. ROOT.ML:100: warning: Value identifier (A_) has not been referenced. ROOT.ML:103: warning: Value identifier (f) has not been referenced. ROOT.ML:128: warning: Matches are not exhaustive. Found near fun the (SOME x2) = x2 ROOT.ML:149: warning: Value identifier (A_) has not been referenced. ROOT.ML:147: warning: Value identifier (x2) has not been referenced. ROOT.ML:147: warning: Value identifier (A_) has not been referenced. ROOT.ML:146: warning: Value identifier (x2) has not been referenced. ROOT.ML:146: warning: Value identifier (A_) has not been referenced. ROOT.ML:158: warning: Value identifier (r) has not been referenced. ROOT.ML:157: warning: Value identifier (y2) has not been referenced. ROOT.ML:157: warning: Value identifier (r) has not been referenced. ROOT.ML:156: warning: Value identifier (y2) has not been referenced. ROOT.ML:156: warning: Value identifier (r) has not been referenced. structure Generated_Code: sig type 'a equal val fBall: 'a fset -> ('a -> bool) -> bool val fmadd: 'a equal -> ('a, 'b) fmap -> ('a, 'b) fmap -> ('a, 'b) fmap type ('a, 'b) fmap val fmcomp: 'a equal -> 'b equal -> ('a, 'c) fmap -> ('b, 'a) fmap -> ('b, 'c) fmap val fmdom: ('a, 'b) fmap -> 'a fset val fmdoma: ('a, 'b) fmap -> 'a set val fmdrop: 'a equal -> 'a -> ('a, 'b) fmap -> ('a, 'b) fmap val fmdrop_fset: 'a equal -> 'a fset -> ('a, 'b) fmap -> ('a, 'b) fmap val fmdrop_set: 'a equal -> 'a set -> ('a, 'b) fmap -> ('a, 'b) fmap val fmempty: ('a, 'b) fmap val fmfilter: ('a -> bool) -> ('a, 'b) fmap -> ('a, 'b) fmap val fmimage: 'a equal -> ('a, 'b) fmap -> 'a fset -> 'b fset val fmlookup: 'a equal -> ('a, 'b) fmap -> 'a -> 'b option val fmmap: ('a -> 'b) -> ('c, 'a) fmap -> ('c, 'b) fmap val fmmap_keys: ('a -> 'b -> 'c) -> ('a, 'b) fmap -> ('a, 'c) fmap val fmpred: 'a equal -> ('a -> 'b -> bool) -> ('a, 'b) fmap -> bool val fmran: 'a equal -> ('a, 'b) fmap -> 'b fset val fmrana: 'a equal -> ('a, 'b) fmap -> 'b set val fmrel: 'a equal -> ('b -> 'c -> bool) -> ('a, 'b) fmap -> ('a, 'c) fmap -> bool val fmrel_on_fset: 'a equal -> 'a fset -> ('b -> 'c -> bool) -> ('a, 'b) fmap -> ('a, 'c) fmap -> bool val fmrestrict_fset: 'a equal -> 'a fset -> ('a, 'b) fmap -> ('a, 'b) fmap val fmrestrict_set: 'a equal -> 'a set -> ('a, 'b) fmap -> ('a, 'b) fmap val fmsubset: 'a equal -> 'b equal -> ('a, 'b) fmap -> ('a, 'b) fmap -> bool val fmupd: 'a equal -> 'a -> 'b -> ('a, 'b) fmap -> ('a, 'b) fmap type 'a fset val pred_fmap: 'a equal -> ('b -> bool) -> ('a, 'b) fmap -> bool type 'a set end ### ISABELLE_OCAMLEXEC not set; skipped checking code for OCaml locale experiment2779892 ### theory "HOL-Library.Finite_Map" ### 15.528s elapsed time, 15.720s cpu time, 0.224s GC time Loading theory "Higher_Order_Terms.Disjoint_Sets" Loading theory "Higher_Order_Terms.Term_Utils" Loading theory "Higher_Order_Terms.Find_First" ### theory "Higher_Order_Terms.Disjoint_Sets" ### 0.110s elapsed time, 0.404s cpu time, 0.000s GC time Found termination order: "(\p. length (snd p)) <*mlex*> {}" Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. length (snd p)) <*mlex*> {}" ### theory "Higher_Order_Terms.Find_First" ### 0.842s elapsed time, 2.628s cpu time, 0.276s GC time ### theory "Higher_Order_Terms.Term_Utils" ### 0.897s elapsed time, 2.840s cpu time, 0.276s GC time Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" Loading theory "Deriving.Derive_Manager" (required by "Higher_Order_Terms.Term_Class" via "Datatype_Order_Generator.Order_Generator" via "Datatype_Order_Generator.Derive_Aux") Loading theory "HOL-Library.Infinite_Set" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util" via "HOL-Library.Extended_Nat" via "HOL-Library.Order_Continuity" via "HOL-Library.Countable_Complete_Lattices" via "HOL-Library.Countable_Set") Loading theory "HOL-Library.Cancellation" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util" via "HOL-Library.Multiset_Order" via "HOL-Library.Multiset") Loading theory "HOL-ex.Unification" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Higher_Order_Terms.Unification_Compat") signature DERIVE_MANAGER = sig val derive: string -> string -> string -> theory -> theory val derive_cmd: string -> string -> string -> theory -> theory val print_info: theory -> unit val register_derive: string -> string -> (string -> string -> theory -> theory) -> theory -> theory end structure Derive_Manager: DERIVE_MANAGER ### theory "Deriving.Derive_Manager" ### 0.072s elapsed time, 0.348s cpu time, 0.000s GC time Loading theory "Datatype_Order_Generator.Derive_Aux" (required by "Higher_Order_Terms.Term_Class" via "Datatype_Order_Generator.Order_Generator") ### Rewrite rule not in simpset: ### \distinct (map fst ?xys3); (?x3, ?y3) \ set ?xys3\ ### \ map_of ?xys3 ?x3 = Some ?y3 \ True ### Rewrite rule not in simpset: ### ?m2.3 ?k3 = Some ?k'3 \ ### (?m1.3 \\<^sub>m ?m2.3) ?k3 = ?m1.3 ?k'3 \ True ### Rewrite rule not in simpset: ### ?n3 ?k3 = Some ?xx3 \ ### (?m3 ++ ?n3) ?k3 = Some ?xx3 \ True ### ML warning (line 140 of "$AFP/Datatype_Order_Generator/derive_aux.ML"): ### Value identifier (sort) has not been referenced. signature DERIVE_AUX = sig val HOLogic_list_all: term list * term -> term val HOLogic_list_conj: term list -> term val HOLogic_list_implies: term list * term -> term val define_overloaded: string * term -> local_theory -> thm * local_theory val define_overloaded_generic: Attrib.binding * term -> local_theory -> thm * local_theory val dt_number_recs: Old_Datatype_Aux.dtyp list -> int * (int * int) list val inductive_thm: theory -> (term list * term list) list -> thm -> sort -> (Proof.context -> int -> thm list -> thm list -> term list -> term list -> tactic) -> thm val mk_Some: term -> term val mk_binary_thm: (theory -> Old_Datatype_Aux.info -> sort -> 'a -> (term list * term list) list) -> (theory -> Old_Datatype_Aux.info -> sort -> (int -> term) * ('b * int * int) list) -> string -> theory -> Old_Datatype_Aux.info -> 'a -> sort -> (Proof.context -> thm list -> thm list -> thm -> (Proof.context -> thm list -> tactic) -> int -> term list -> term list -> string * Old_Datatype_Aux.dtyp list -> (Old_Datatype_Aux.dtyp -> term -> ...) -> tactic) -> thm val mk_case_tac: Proof.context -> term option list list -> thm -> (Proof.context * int * thm list * (string * cterm) list -> tactic) -> tactic val mk_def: typ -> string -> term -> term val mk_solve_with_tac: Proof.context -> thm list -> tactic -> tactic val mk_xs: theory -> Old_Datatype_Aux.info -> sort -> int -> int -> term val my_print_tac: Proof.context -> string -> tactic val my_simp_set: simpset val prop_trm_to_major_imp: (term list * 'a) list -> term * 'a val rulify_only_asm: Proof.context -> thm -> thm val split_last: 'a list -> 'a list * 'a val typ_and_vs_of_typname: theory -> string -> sort -> typ * (string * sort) list val typ_subst_for_sort: theory -> Old_Datatype_Aux.info -> sort -> typ -> typ end structure Derive_Aux: DERIVE_AUX ### theory "Datatype_Order_Generator.Derive_Aux" ### 0.253s elapsed time, 0.996s cpu time, 0.000s GC time Loading theory "Datatype_Order_Generator.Order_Generator" (required by "Higher_Order_Terms.Term_Class") consts enumerate :: "'a set \ nat \ 'a" ### theory "HOL-Library.Infinite_Set" ### 0.443s elapsed time, 1.812s cpu time, 0.000s GC time Loading theory "HOL-Library.Countable_Set" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util" via "HOL-Library.Extended_Nat" via "HOL-Library.Order_Continuity" via "HOL-Library.Countable_Complete_Lattices") ### 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 ### ML warning (line 134 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 140 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 146 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 211 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 173 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 307 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 318 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 363 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 382 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 397 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 430 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 438 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 474 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Matches are not exhaustive. ### ML warning (line 524 of "$AFP/Datatype_Order_Generator/order_generator.ML"): ### Pattern is not exhaustive. signature ORDER_GENERATOR = sig val derive: int -> string -> string -> theory -> theory val mk_antisym_thm: theory -> Old_Datatype_Aux.info -> thm -> thm -> thm val mk_le_refl_thm: theory -> Old_Datatype_Aux.info -> thm val mk_less_eq_idx: theory -> Old_Datatype_Aux.info -> sort -> int -> term -> term -> term val mk_less_idx: theory -> Old_Datatype_Aux.info -> sort -> (int -> term) * (term * int * int) list val mk_less_le_not_le_thm: theory -> Old_Datatype_Aux.info -> thm val mk_linear_thm: theory -> Old_Datatype_Aux.info -> thm val mk_order_thms: theory -> Old_Datatype_Aux.info -> thm list val mk_transitivity_thms: theory -> Old_Datatype_Aux.info -> thm * thm end structure Order_Generator: ORDER_GENERATOR ### theory "Datatype_Order_Generator.Order_Generator" ### 0.303s elapsed time, 1.216s cpu time, 0.000s GC time Loading theory "Higher_Order_Terms.Fresh_Monad" 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 locale fresh fixes "next" :: "'a \ 'a" and arb :: "'a" assumes "fresh next" ### theory "Higher_Order_Terms.Fresh_Monad" ### 0.152s elapsed time, 0.612s cpu time, 0.000s GC time Loading theory "Higher_Order_Terms.Name" 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.862s elapsed time, 3.488s cpu time, 0.000s GC time Loading theory "HOL-Library.Multiset" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util" via "HOL-Library.Multiset_Order") ### theory "HOL-Library.Countable_Set" ### 0.736s elapsed time, 2.876s cpu time, 0.588s GC time Loading theory "HOL-Library.Countable_Complete_Lattices" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util" via "HOL-Library.Extended_Nat" via "HOL-Library.Order_Continuity") consts vars_of :: "'a trm \ 'a set" 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 Found termination order: "(\p. size (snd p)) <*mlex*> {}" instantiation name :: ord less_eq_name == less_eq :: name \ name \ bool less_name == less :: name \ name \ bool Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" consts subst :: "'a trm \ ('a \ 'a trm) list \ 'a trm" ### theory "Higher_Order_Terms.Name" ### 0.729s elapsed time, 2.840s cpu time, 0.588s GC time Loading theory "Higher_Order_Terms.Fresh_Class" class countable_complete_lattice = Inf + Sup + lattice + bot + top + assumes "ccInf_lower": "\A x. \countable A; x \ A\ \ Inf A \ x" assumes "ccInf_greatest": "\A z. \countable A; \x. x \ A \ z \ x\ \ z \ Inf A" assumes "ccSup_upper": "\A x. \countable A; x \ A\ \ x \ Sup A" assumes "ccSup_least": "\A z. \countable A; \x. x \ A \ x \ z\ \ Sup A \ z" assumes "ccInf_empty": "Inf {} = top" assumes "ccSup_empty": "Sup {} = bot" Found termination order: "(\p. size_list (\p. size (snd p)) (fst p)) <*mlex*> {}" ### Partially applied constant "Multiset.inf_subset_mset" on left hand side of equation, in theorem: ### semilattice_inf.Inf_fin (\#) (set (?x # ?xs)) \ ### fold (\#) ?xs ?x ### Partially applied constant "Multiset.sup_subset_mset" on left hand side of equation, in theorem: ### semilattice_sup.Sup_fin (\#) (set (?x # ?xs)) \ ### fold (\#) ?xs ?x ### theory "HOL-ex.Unification" ### 2.374s elapsed time, 9.436s cpu time, 0.588s GC time Loading theory "Higher_Order_Terms.Term_Class" class fresh = default + linorder + fixes "next" :: "'a \ 'a" assumes "next_ge": "\x. x < next x" Found termination order: "(\p. size (fst p)) <*mlex*> {}" instantiation nat :: fresh next_nat == next :: nat \ nat default_nat == default :: nat instantiation char :: default default_char == default :: char instantiation name :: fresh next_name == next :: name \ name default_name == default :: name 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 class countable_complete_distrib_lattice = countable_complete_lattice + assumes "sup_ccInf": "\B a. countable B \ sup a (Inf B) = Inf (sup a ` B)" assumes "inf_ccSup": "\B a. countable B \ inf a (Sup B) = Sup (inf a ` B)" instantiation multiset :: (type) size size_multiset == size :: 'a multiset \ nat locale comp_fun_commute fixes f :: "'a \ 'b \ 'b" assumes "comp_fun_commute f" consts mset :: "'a list \ 'a multiset" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" locale comm_monoid_mset fixes f :: "'a \ 'a \ 'a" (infixl \\<^bold>*\ 70) and z :: "'a" (\\<^bold>1\) assumes "comm_monoid_mset (\<^bold>*) \<^bold>1" class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" ### theory "HOL-Library.Countable_Complete_Lattices" ### 2.840s elapsed time, 10.072s cpu time, 0.516s GC time Loading theory "HOL-Library.Order_Continuity" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util" via "HOL-Library.Extended_Nat") class canonically_ordered_monoid_add = ordered_comm_monoid_add + assumes "le_iff_add": "\a b. (a \ b) = (\c. b = a + c)" creating orders for datatype term class comm_monoid_mult = ab_semigroup_mult + monoid_mult + dvd + assumes "mult_1": "\a. (1::'a) * a = a" registered term in class ord registered term in class order registered term in class linorder class pre_term = size + fixes frees :: "'a \ name fset" and subst :: "'a \ (name, 'a) fmap \ 'a" and "consts" :: "'a \ name fset" and app :: "'a \ 'a \ 'a" and unapp :: "'a \ ('a \ 'a) option" and const :: "name \ 'a" and unconst :: "'a \ name option" and free :: "name \ 'a" and unfree :: "'a \ name option" assumes "unapp_app": "\u\<^sub>1 u\<^sub>2. unapp (app u\<^sub>1 u\<^sub>2) = Some (u\<^sub>1, u\<^sub>2)" assumes "app_unapp": "\u u\<^sub>1 u\<^sub>2. unapp u = Some (u\<^sub>1, u\<^sub>2) \ u = app u\<^sub>1 u\<^sub>2" assumes "app_size": "\u\<^sub>1 u\<^sub>2. size (app u\<^sub>1 u\<^sub>2) = size u\<^sub>1 + size u\<^sub>2 + 1" assumes "unconst_const": "\name. unconst (const name) = Some name" assumes "const_unconst": "\u name. unconst u = Some name \ u = const name" assumes "unfree_free": "\name. unfree (free name) = Some name" assumes "free_unfree": "\u name. unfree u = Some name \ u = free name" assumes "app_const_distinct": "\u\<^sub>1 u\<^sub>2 name. app u\<^sub>1 u\<^sub>2 \ const name" assumes "app_free_distinct": "\u\<^sub>1 u\<^sub>2 name. app u\<^sub>1 u\<^sub>2 \ free name" assumes "free_const_distinct": "\name\<^sub>1 name\<^sub>2. free name\<^sub>1 \ const name\<^sub>2" assumes "frees_const": "\name. frees (const name) = {||}" assumes "frees_free": "\name. frees (free name) = {|name|}" assumes "frees_app": "\u\<^sub>1 u\<^sub>2. frees (app u\<^sub>1 u\<^sub>2) = frees u\<^sub>1 |\| frees u\<^sub>2" assumes "consts_free": "\name. consts (free name) = {||}" assumes "consts_const": "\name. consts (const name) = {|name|}" assumes "consts_app": "\u\<^sub>1 u\<^sub>2. consts (app u\<^sub>1 u\<^sub>2) = consts u\<^sub>1 |\| consts u\<^sub>2" assumes "subst_app": "\u\<^sub>1 u\<^sub>2 env. subst (app u\<^sub>1 u\<^sub>2) env = app (subst u\<^sub>1 env) (subst u\<^sub>2 env)" assumes "subst_const": "\name env. subst (const name) env = const name" assumes "subst_free": "\name env. subst (free name) env = (case fmlookup env name of None \ free name | Some t \ t)" assumes "free_inject": "\name\<^sub>1 name\<^sub>2. free name\<^sub>1 = free name\<^sub>2 \ name\<^sub>1 = name\<^sub>2" assumes "const_inject": "\name\<^sub>1 name\<^sub>2. const name\<^sub>1 = const name\<^sub>2 \ name\<^sub>1 = name\<^sub>2" assumes "app_inject": "\u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4. app u\<^sub>1 u\<^sub>2 = app u\<^sub>3 u\<^sub>4 \ u\<^sub>1 = u\<^sub>3 \ u\<^sub>2 = u\<^sub>4" instantiation term :: pre_term frees_term == frees :: term \ name fset subst_term == subst :: term \ (name, term) fmap \ term consts_term == consts :: term \ name fset app_term == app :: term \ term \ term unapp_term == unapp :: term \ (term \ term) option const_term == const :: name \ term unconst_term == unconst :: term \ name option free_term == free :: name \ term unfree_term == unfree :: term \ name option Found termination order: "{}" ### theory "HOL-Library.Order_Continuity" ### 0.817s elapsed time, 2.460s cpu time, 0.000s GC time Loading theory "HOL-Library.Extended_Nat" (required by "Higher_Order_Terms.Lambda_Free_Compat" via "Lambda_Free_RPOs.Lambda_Free_Term" via "Lambda_Free_RPOs.Lambda_Free_Util") Found termination order: "{}" class infinity = type + fixes infinity :: "'a" instantiation enat :: infinity infinity_enat == infinity :: enat Proofs for inductive predicate(s) "rec_set_enat" Proving monotonicity ... Proving the introduction rules ... class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Proving the elimination rules ... Found termination order: "{}" Proving the simplification rules ... Found termination order: "size <*mlex*> {}" ### No equation for constructor "Extended_Nat.infinity_class.infinity" ### in definition of function "the_enat" Found termination order: "(\p. size (fst p)) <*mlex*> {}" consts the_enat :: "enat \ nat" instantiation enat :: zero_neq_one one_enat == one_class.one :: enat zero_enat == zero_class.zero :: enat instantiation multiset :: (preorder) order less_eq_multiset == less_eq :: 'a multiset \ 'a multiset \ bool less_multiset == less :: 'a multiset \ 'a multiset \ bool instantiation enat :: comm_monoid_add plus_enat == plus :: enat \ enat \ enat instantiation enat :: {comm_semiring_1,semiring_no_zero_divisors} times_enat == times :: enat \ enat \ enat instantiation multiset :: (preorder) ordered_ab_semigroup_add Found termination order: "size <*mlex*> {}" Proofs for inductive predicate(s) "pw_leq" class pre_term = size + fixes frees :: "'a \ name fset" and subst :: "'a \ (name, 'a) fmap \ 'a" and "consts" :: "'a \ name fset" and app :: "'a \ 'a \ 'a" and unapp :: "'a \ ('a \ 'a) option" and const :: "name \ 'a" and unconst :: "'a \ name option" and free :: "name \ 'a" and unfree :: "'a \ name option" assumes "unapp_app": "\u\<^sub>1 u\<^sub>2. unapp (app u\<^sub>1 u\<^sub>2) = Some (u\<^sub>1, u\<^sub>2)" assumes "app_unapp": "\u u\<^sub>1 u\<^sub>2. unapp u = Some (u\<^sub>1, u\<^sub>2) \ u = app u\<^sub>1 u\<^sub>2" assumes "app_size": "\u\<^sub>1 u\<^sub>2. size (app u\<^sub>1 u\<^sub>2) = size u\<^sub>1 + size u\<^sub>2 + 1" assumes "unconst_const": "\name. unconst (const name) = Some name" assumes "const_unconst": "\u name. unconst u = Some name \ u = const name" assumes "unfree_free": "\name. unfree (free name) = Some name" assumes "free_unfree": "\u name. unfree u = Some name \ u = free name" assumes "app_const_distinct": "\u\<^sub>1 u\<^sub>2 name. app u\<^sub>1 u\<^sub>2 \ const name" assumes "app_free_distinct": "\u\<^sub>1 u\<^sub>2 name. app u\<^sub>1 u\<^sub>2 \ free name" assumes "free_const_distinct": "\name\<^sub>1 name\<^sub>2. free name\<^sub>1 \ const name\<^sub>2" assumes "frees_const": "\name. frees (const name) = {||}" assumes "frees_free": "\name. frees (free name) = {|name|}" assumes "frees_app": "\u\<^sub>1 u\<^sub>2. frees (app u\<^sub>1 u\<^sub>2) = frees u\<^sub>1 |\| frees u\<^sub>2" assumes "consts_free": "\name. consts (free name) = {||}" assumes "consts_const": "\name. consts (const name) = {|name|}" assumes "consts_app": "\u\<^sub>1 u\<^sub>2. consts (app u\<^sub>1 u\<^sub>2) = consts u\<^sub>1 |\| consts u\<^sub>2" assumes "subst_app": "\u\<^sub>1 u\<^sub>2 env. subst (app u\<^sub>1 u\<^sub>2) env = app (subst u\<^sub>1 env) (subst u\<^sub>2 env)" assumes "subst_const": "\name env. subst (const name) env = const name" assumes "subst_free": "\name env. subst (free name) env = (case fmlookup env name of None \ free name | Some t \ t)" assumes "free_inject": "\name\<^sub>1 name\<^sub>2. free name\<^sub>1 = free name\<^sub>2 \ name\<^sub>1 = name\<^sub>2" assumes "const_inject": "\name\<^sub>1 name\<^sub>2. const name\<^sub>1 = const name\<^sub>2 \ name\<^sub>1 = name\<^sub>2" assumes "app_inject": "\u\<^sub>1 u\<^sub>2 u\<^sub>3 u\<^sub>4. app u\<^sub>1 u\<^sub>2 = app u\<^sub>3 u\<^sub>4 \ u\<^sub>1 = u\<^sub>3 \ u\<^sub>2 = u\<^sub>4" Proving monotonicity ... instantiation enat :: minus minus_enat == minus :: enat \ enat \ enat Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation enat :: linordered_ab_semigroup_add less_eq_enat == less_eq :: enat \ enat \ bool less_enat == less :: enat \ enat \ bool instantiation enat :: {order_bot,order_top} top_enat == top :: enat bot_enat == bot :: enat structure Cancel_Enat_Common: sig val dest_sum: term -> term list val dest_summing: term * term list -> term list val find_first: term -> term list -> term list val find_first_t: term list -> term -> term list -> term list val mk_eq: term * term -> term val mk_sum: typ -> term list -> term val norm_ss: simpset val norm_tac: Proof.context -> tactic val simplify_meta_eq: Proof.context -> thm -> thm -> thm val trans_tac: Proof.context -> thm option -> tactic end structure Eq_Enat_Cancel: sig val proc: Proof.context -> term -> thm option end structure Le_Enat_Cancel: sig val proc: Proof.context -> term -> thm option end structure Less_Enat_Cancel: sig val proc: Proof.context -> term -> thm option end instantiation enat :: complete_lattice Inf_enat == Inf :: enat set \ enat Sup_enat == Sup :: enat set \ enat sup_enat == sup :: enat \ enat \ enat inf_enat == inf :: enat \ enat \ enat Found termination order: "(\p. length (fst p)) <*mlex*> {}" instantiation multiset :: (equal) equal equal_multiset == equal_class.equal :: 'a multiset \ 'a multiset \ bool ### theory "HOL-Library.Extended_Nat" ### 1.128s elapsed time, 3.524s cpu time, 0.648s GC time instantiation multiset :: (random) random random_multiset == random_class.random :: natural \ natural \ natural \ ('a multiset \ (unit \ term)) \ natural \ natural class term = pre_term + fixes abs_pred :: "('a \ bool) \ 'a \ bool" assumes "raw_induct": "\P t. \\name. P (const name); \name. P (free name); \t\<^sub>1 t\<^sub>2. \P t\<^sub>1; P t\<^sub>2\ \ P (app t\<^sub>1 t\<^sub>2); \t. abs_pred P t\ \