Loading theory "Containers.Equal" (required by "Containers.Containers") Loading theory "Containers.Extend_Partial_Order" (required by "Containers.Set_Linorder") locale equal_base fixes equal :: "'a \ 'a \ bool" locale Equal.equal fixes equal :: "'a \ 'a \ bool" assumes "equal equal" ### theory "Containers.Equal" ### 0.042s elapsed time, 0.124s cpu time, 0.000s GC time Loading theory "Containers.Closure_Set" (required by "Containers.Containers" via "Containers.Mapping_Impl" via "Containers.Set_Impl") locale equal_base fixes equal :: "'a \ 'a \ bool" ### theory "Containers.Closure_Set" ### 0.042s elapsed time, 0.124s cpu time, 0.000s GC time Loading theory "Containers.List_Fusion" (required by "Containers.Set_Linorder" via "Containers.Lexicographic_Order") Proofs for inductive predicate(s) "terminates_onp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Containers.Extend_Partial_Order" ### 0.236s elapsed time, 0.552s cpu time, 0.000s GC time Loading theory "Containers.AssocList" (required by "Containers.Containers" via "Containers.Mapping_Impl") consts update_with_aux :: "'val \ 'key \ ('val \ 'val) \ ('key \ 'val) list \ ('key \ 'val) list" Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" locale list fixes g :: "('a, 's) generator" consts list_has_next :: "'a list \ bool" ### No equation for constructor "[]" consts list_next :: "'a list \ 'a \ 'a list" ### theory "Containers.AssocList" ### 0.452s elapsed time, 0.904s cpu time, 0.000s GC time Loading theory "Containers.Containers_Auxiliary" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Found termination order: "{}" ### Dropping global mixfix syntax: "less_eq_prod" (infix "\" 50) ### Dropping global mixfix syntax: "less_prod" (infix "\" 50) ### Dropping global mixfix syntax: "less_eq_prod'" (infix "\" 50) ### Dropping global mixfix syntax: "less_prod'" (infix "\" 50) ### theory "Containers.Containers_Auxiliary" ### 0.328s elapsed time, 0.660s cpu time, 0.000s GC time Loading theory "Containers.Containers_Generator" (required by "Containers.Collection_Order") Found termination order: "case_sum (\x. Suc 0) (\x. 0) <*mlex*> {}" Proofs for inductive predicate(s) "filter_has_next" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... signature CONTAINERS_GENERATOR = sig val HOLogic_list_conj: term list -> term val all_tys: term -> typ list -> term -> term val derive_is_c_dots_lemma: typ -> string -> thm list -> string -> theory -> theory val derive_none: string -> sort -> (typ -> term) -> string -> theory -> theory val derive_set_map_impl: string -> sort -> (string * term) list -> string -> string -> theory -> theory val is_class_instance: theory -> string -> sort -> bool val mk_Some: term -> term val mk_is_c_dots: typ -> string -> term val register_is_c_dots_lemma: string -> string -> thm -> theory -> theory end structure Containers_Generator: CONTAINERS_GENERATOR ### theory "Containers.Containers_Generator" ### 0.609s elapsed time, 1.208s cpu time, 0.000s GC time Loading theory "Containers.Collection_Enum" (required by "Containers.Containers") class cenum = type + fixes cEnum :: "('a list \ (('a \ bool) \ bool) \ (('a \ bool) \ bool)) option" assumes "UNIV_cenum": "\enum enum_all enum_ex. cEnum = Some (enum, enum_all, enum_ex) \ UNIV = set enum" and "cenum_all_UNIV": "\enum enum_all enum_ex P. cEnum = Some (enum, enum_all, enum_ex) \ enum_all P = Ball UNIV P" and "cenum_ex_UNIV": "\enum enum_all enum_ex P. cEnum = Some (enum, enum_all, enum_ex) \ enum_ex P = Bex UNIV P" ### theory "Containers.List_Fusion" ### 1.662s elapsed time, 3.316s cpu time, 0.000s GC time Loading theory "Containers.Lexicographic_Order" (required by "Containers.Set_Linorder") signature CENUM_GENERATOR = sig val derive_no_cenum: string -> theory -> theory end structure Cenum_Generator: CENUM_GENERATOR ### Rewrite rule not in simpset: ### Wellfounded.accp all_n_lists_rel (?P1, ?n1) \ ### all_n_lists ?P1 ?n1 \ ### if ?n1 = 0 then ?P1 [] ### else cenum_all ### (\x. all_n_lists (\xs. ?P1 (x # xs)) (?n1 - 1)) Found termination order: "(\p. size (snd p)) <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" ### Rewrite rule not in simpset: ### Wellfounded.accp ex_n_lists_rel (?P1, ?n1) \ ### ex_n_lists ?P1 ?n1 \ ### if ?n1 = 0 then ?P1 [] ### else cenum_ex (\x. ex_n_lists (\xs. ?P1 (x # xs)) (?n1 - 1)) Found termination order: "(\p. size (snd p)) <*mlex*> {}" instantiation fun :: (cenum, cenum) cenum cEnum_fun == cEnum :: (('a \ 'b) list \ ((('a \ 'b) \ bool) \ bool) \ ((('a \ 'b) \ bool) \ bool)) option ### theory "Containers.Lexicographic_Order" ### 0.594s elapsed time, 1.124s cpu time, 0.424s GC time Loading theory "Containers.Collection_Eq" (required by "Containers.Containers") ### Ambiguous input (line 136 of "~~/afp/thys/Containers/Collection_Enum.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_CENUM" ("\<^type>fun" ("_position_sort" 'a) ("_position_sort" 'b))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'a))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_a) ### ("_tuple_args" ("_position" enum_all_a) ### ("_tuple_arg" ("_position" enum_ex_a))))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'b))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_b) ### ("_tuple_args" ("_position" enum_all_b) ### ("_tuple_arg" ("_position" enum_ex_b))))) ### ("_applC" ("_position" Some) ### ("_tuple" ### ("_applC" ("_position" map) ### ("_cargs" ### ("_lambda" ("_position" ys) ### ("\<^const>Fun.comp" ("_position" the) ### ("_applC" ("_position" map_of) ### ("_applC" ("_position" zip) ### ("_cargs" ("_position" enum_a) ### ("_position" ys)))))) ### ("_applC" ("_position" List.n_lists) ### ("_cargs" ### ("_applC" ("_position" length) ### ("_position" enum_a)) ### ("_position" enum_b))))) ### ("_tuple_args" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" all_n_lists) ### ("_cargs" ("_position" enum_all_b) ### ("_cargs" ### ("_lambda" ("_position" bs) ### ("_applC" ("_position" P) ### ("\<^const>Fun.comp" ("_position" the) ### ("_applC" ("_position" map_of) ### ("_applC" ("_position" zip) ### ("_cargs" ("_position" enum_a) ("_position" bs))))))) ### ("_applC" ("_position" length) ### ("_position" enum_a)))))) ### ("_tuple_arg" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" ex_n_lists) ### ("_cargs" ("_position" enum_ex_b) ### ("_cargs" ### ("_lambda" ("_position" bs) ### ("_applC" ("_position" P) ### ("\<^const>Fun.comp" ("_position" the) ### ("_applC" ("_position" map_of) ### ("_applC" ("_position" zip) ### ("_cargs" ("_position" enum_a) ("_position" bs))))))) ### ("_applC" ("_position" length) ### ("_position" enum_a)))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_CENUM" ("\<^type>fun" ("_position_sort" 'a) ("_position_sort" 'b))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'a))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_a) ### ("_tuple_args" ("_position" enum_all_a) ### ("_tuple_arg" ("_position" enum_ex_a))))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ("_position" None)))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_b) ### ("_tuple_args" ("_position" enum_all_b) ### ("_tuple_arg" ("_position" enum_ex_b))))) ### ("_applC" ("_position" Some) ### ("_tuple" ### ("_applC" ("_position" map) ### ("_cargs" ### ("_lambda" ("_position" ys) ### ("\<^const>Fun.comp" ("_position" the) ### ("_applC" ("_position" map_of) ### ("_applC" ("_position" zip) ### ("_cargs" ("_position" enum_a) ### ("_position" ys)))))) ### ("_applC" ("_position" List.n_lists) ### ("_cargs" ### ("_applC" ("_position" length) ("_position" enum_a)) ### ("_position" enum_b))))) ### ("_tuple_args" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" all_n_lists) ### ("_cargs" ("_position" enum_all_b) ### ("_cargs" ### ("_lambda" ("_position" bs) ### ("_applC" ("_position" P) ### ("\<^const>Fun.comp" ("_position" the) ### ("_applC" ("_position" map_of) ### ("_applC" ("_position" zip) ### ("_cargs" ("_position" enum_a) ### ("_position" bs))))))) ### ("_applC" ("_position" length) ### ("_position" enum_a)))))) ### ("_tuple_arg" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" ex_n_lists) ### ("_cargs" ("_position" enum_ex_b) ### ("_cargs" ### ("_lambda" ("_position" bs) ### ("_applC" ("_position" P) ### ("\<^const>Fun.comp" ("_position" the) ### ("_applC" ("_position" map_of) ### ("_applC" ("_position" zip) ### ("_cargs" ("_position" enum_a) ("_position" bs))))))) ### ("_applC" ("_position" length) ### ("_position" enum_a)))))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. instantiation set :: (cenum) cenum cEnum_set == cEnum :: ('a set list \ (('a set \ bool) \ bool) \ (('a set \ bool) \ bool)) option instantiation unit :: cenum cEnum_unit == cEnum :: (unit list \ ((unit \ bool) \ bool) \ ((unit \ bool) \ bool)) option instantiation bool :: cenum cEnum_bool == cEnum :: (bool list \ ((bool \ bool) \ bool) \ ((bool \ bool) \ bool)) option instantiation prod :: (cenum, cenum) cenum cEnum_prod == cEnum :: (('a \ 'b) list \ (('a \ 'b \ bool) \ bool) \ (('a \ 'b \ bool) \ bool)) option ### Ambiguous input (line 225 of "~~/afp/thys/Containers/Collection_Enum.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_CENUM" ### ("\<^type>Product_Type.prod" ("_position_sort" 'a) ### ("_position_sort" 'b))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'a))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_a) ### ("_tuple_args" ("_position" enum_all_a) ### ("_tuple_arg" ("_position" enum_ex_a))))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'b))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_b) ### ("_tuple_args" ("_position" enum_all_b) ### ("_tuple_arg" ("_position" enum_ex_b))))) ### ("_applC" ("_position" Some) ### ("_tuple" ### ("_applC" ("_position" List.product) ### ("_cargs" ("_position" enum_a) ("_position" enum_b))) ### ("_tuple_args" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" enum_all_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" enum_all_b) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" P) ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" y))))))))) ### ("_tuple_arg" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" enum_ex_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" enum_ex_b) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" P) ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" y))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_CENUM" ### ("\<^type>Product_Type.prod" ("_position_sort" 'a) ### ("_position_sort" 'b))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'a))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_a) ### ("_tuple_args" ("_position" enum_all_a) ### ("_tuple_arg" ("_position" enum_ex_a))))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ("_position" None)))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_b) ### ("_tuple_args" ("_position" enum_all_b) ### ("_tuple_arg" ("_position" enum_ex_b))))) ### ("_applC" ("_position" Some) ### ("_tuple" ### ("_applC" ("_position" List.product) ### ("_cargs" ("_position" enum_a) ("_position" enum_b))) ### ("_tuple_args" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" enum_all_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" enum_all_b) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" P) ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" y))))))))) ### ("_tuple_arg" ### ("_lambda" ("_position" P) ### ("_applC" ("_position" enum_ex_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" enum_ex_b) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" P) ### ("_tuple" ("_position" x) ### ("_tuple_arg" ### ("_position" y))))))))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. instantiation sum :: (cenum, cenum) cenum cEnum_sum == cEnum :: (('a + 'b) list \ (('a + 'b \ bool) \ bool) \ (('a + 'b \ bool) \ bool)) option ### Ambiguous input (line 237 of "~~/afp/thys/Containers/Collection_Enum.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_CENUM" ### ("\<^type>Sum_Type.sum" ("_position_sort" 'a) ("_position_sort" 'b))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'a))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_a) ### ("_tuple_args" ("_position" enum_all_a) ### ("_tuple_arg" ("_position" enum_ex_a))))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'b))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_b) ### ("_tuple_args" ("_position" enum_all_b) ### ("_tuple_arg" ("_position" enum_ex_b))))) ### ("_applC" ("_position" Some) ### ("_tuple" ### ("\<^const>List.append" ### ("_applC" ("_position" map) ### ("_cargs" ("_position" Inl) ("_position" enum_a))) ### ("_applC" ("_position" map) ### ("_cargs" ("_position" Inr) ("_position" enum_b)))) ### ("_tuple_args" ### ("_lambda" ("_position" P) ### ("\<^const>HOL.conj" ### ("_applC" ("_position" enum_all_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inl) ### ("_position" x))))) ### ("_applC" ("_position" enum_all_b) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inr) ### ("_position" x))))))) ### ("_tuple_arg" ### ("_lambda" ("_position" P) ### ("\<^const>HOL.disj" ### ("_applC" ("_position" enum_ex_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inl) ### ("_position" x))))) ### ("_applC" ("_position" enum_ex_b) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inr) ### ("_position" x))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_CENUM" ### ("\<^type>Sum_Type.sum" ("_position_sort" 'a) ("_position_sort" 'b))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'a))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_a) ### ("_tuple_args" ("_position" enum_all_a) ### ("_tuple_arg" ("_position" enum_ex_a))))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CENUM" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ("_position" None)))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" enum_b) ### ("_tuple_args" ("_position" enum_all_b) ### ("_tuple_arg" ("_position" enum_ex_b))))) ### ("_applC" ("_position" Some) ### ("_tuple" ### ("\<^const>List.append" ### ("_applC" ("_position" map) ### ("_cargs" ("_position" Inl) ("_position" enum_a))) ### ("_applC" ("_position" map) ### ("_cargs" ("_position" Inr) ("_position" enum_b)))) ### ("_tuple_args" ### ("_lambda" ("_position" P) ### ("\<^const>HOL.conj" ### ("_applC" ("_position" enum_all_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inl) ("_position" x))))) ### ("_applC" ("_position" enum_all_b) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inr) ### ("_position" x))))))) ### ("_tuple_arg" ### ("_lambda" ("_position" P) ### ("\<^const>HOL.disj" ### ("_applC" ("_position" enum_ex_a) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inl) ### ("_position" x))))) ### ("_applC" ("_position" enum_ex_b) ### ("_lambda" ("_position" x) ### ("_applC" ("_position" P) ### ("_applC" ("_position" Inr) ### ("_position" x))))))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. class ceq = type + fixes ceq :: "('a \ 'a \ bool) option" assumes "ceq": "\eqa. ceq = Some eqa \ eqa = (=)" instantiation option :: (cenum) cenum cEnum_option == cEnum :: ('a option list \ (('a option \ bool) \ bool) \ (('a option \ bool) \ bool)) option instantiation Enum.finite_1 :: cenum cEnum_finite_1 == cEnum :: (Enum.finite_1 list \ ((Enum.finite_1 \ bool) \ bool) \ ((Enum.finite_1 \ bool) \ bool)) option instantiation Enum.finite_2 :: cenum cEnum_finite_2 == cEnum :: (Enum.finite_2 list \ ((Enum.finite_2 \ bool) \ bool) \ ((Enum.finite_2 \ bool) \ bool)) option instantiation Enum.finite_3 :: cenum cEnum_finite_3 == cEnum :: (Enum.finite_3 list \ ((Enum.finite_3 \ bool) \ bool) \ ((Enum.finite_3 \ bool) \ bool)) option instantiation Enum.finite_4 :: cenum cEnum_finite_4 == cEnum :: (Enum.finite_4 list \ ((Enum.finite_4 \ bool) \ bool) \ ((Enum.finite_4 \ bool) \ bool)) option signature CEQ_GENERATOR = sig val ceq_instance_via_eq: string -> theory -> theory val ceq_instance_via_equality: string -> theory -> theory val derive_no_ceq: string -> theory -> theory end structure Ceq_Generator: CEQ_GENERATOR deriving "ceq" instance for type "Product_Type.unit" via "=" instantiation Enum.finite_5 :: cenum cEnum_finite_5 == cEnum :: (Enum.finite_5 list \ ((Enum.finite_5 \ bool) \ bool) \ ((Enum.finite_5 \ bool) \ bool)) option derived is_ceq_unit-lemma ### Code generator: dropping subsumed code equation ### CEQ(unit) \ Some (=) deriving "ceq" instance for type "HOL.bool" via "=" instantiation char :: cenum cEnum_char == cEnum :: (char list \ ((char \ bool) \ bool) \ ((char \ bool) \ bool)) option derived is_ceq_bool-lemma deriving "ceq" instance for type "Nat.nat" via "=" use None as trivial implementation of cenum for type list derived is_ceq_nat-lemma deriving "ceq" instance for type "Int.int" via "=" registered list in class cenum use None as trivial implementation of cenum for type nat derived is_ceq_int-lemma deriving "ceq" instance for type "Enum.finite_1" via "=" registered nat in class cenum use None as trivial implementation of cenum for type int derived is_ceq_finite_1-lemma deriving "ceq" instance for type "Enum.finite_2" via "=" registered int in class cenum use None as trivial implementation of cenum for type integer derived is_ceq_finite_2-lemma deriving "ceq" instance for type "Enum.finite_3" via "=" registered integer in class cenum use None as trivial implementation of cenum for type natural derived is_ceq_finite_3-lemma deriving "ceq" instance for type "Enum.finite_4" via "=" registered natural in class cenum use None as trivial implementation of cenum for type literal derived is_ceq_finite_4-lemma deriving "ceq" instance for type "Enum.finite_5" via "=" registered literal in class cenum ### theory "Containers.Collection_Enum" ### 1.111s elapsed time, 2.160s cpu time, 0.424s GC time Loading theory "Containers.Card_Datatype" derived is_ceq_finite_5-lemma deriving "ceq" instance for type "Code_Numeral.integer" via "=" derived is_ceq_integer-lemma deriving "ceq" instance for type "Code_Numeral.natural" via "=" derived is_ceq_natural-lemma deriving "ceq" instance for type "String.char" via "=" derived is_ceq_char-lemma deriving "ceq" instance for type "String.literal" via "=" derived is_ceq_literal-lemma deriving "ceq" instance for type "Sum_Type.sum" derived is_ceq_sum-lemma deriving "ceq" instance for type "Product_Type.prod" derived is_ceq_prod-lemma deriving "ceq" instance for type "List.list" derived is_ceq_list-lemma deriving "ceq" instance for type "Option.option" structure Card_Simp_Rules: NAMED_THMS derived is_ceq_option-lemma use None as trivial implementation of ceq for type fun registered fun in class ceq instantiation set :: (ceq) ceq ceq_set == ceq :: ('a set \ 'a set \ bool) option ### theory "Containers.Card_Datatype" ### 0.176s elapsed time, 0.352s cpu time, 0.000s GC time Loading theory "Containers.Set_Linorder" instantiation Predicate.pred :: (ceq) ceq ceq_pred == ceq :: ('a Predicate.pred \ 'a Predicate.pred \ bool) option ### theory "Containers.Collection_Eq" ### 0.692s elapsed time, 1.392s cpu time, 0.000s GC time Loading theory "Containers.DList_Set" (required by "Containers.Containers" via "Containers.Mapping_Impl" via "Containers.Set_Impl") locale equal_base fixes equal :: "'a \ 'a \ bool" consts list_member :: "'a list \ 'a \ bool" consts list_distinct :: "'a list \ bool" consts list_remove1 :: "'a \ 'a list \ 'a list" consts list_remdups :: "'a list \ 'a list" locale Equal.equal fixes equal :: "'a \ 'a \ bool" assumes "equal equal" specification finite_complement_partition: finite ?A \ ?A \ infinite_complement_partition complement_partition: infinite UNIV \ (?A \ infinite_complement_partition) = (- ?A \ infinite_complement_partition) class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" class order = preorder + assumes "antisym": "\x y. \x \ y; y \ x\ \ x = y" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "Containers.DList_Set" ### 0.862s elapsed time, 1.724s cpu time, 0.000s GC time Loading theory "Containers.RBT_ext" (required by "Containers.Containers" via "Containers.Mapping_Impl" via "Containers.RBT_Mapping2") class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class proper_intrvl = ord + fixes proper_interval :: "'a option \ 'a option \ bool" ### Dropping global mixfix syntax: "less_eq_prod'" (infix "\" 50) ### Dropping global mixfix syntax: "less_prod'" (infix "\" 50) class proper_interval = proper_intrvl + assumes "proper_interval_simps": "proper_interval None None = True" "\y. proper_interval None (Some y) = (\z. z < y)" "\x. proper_interval (Some x) None = (\z. x < z)" "\x y. proper_interval (Some x) (Some y) = (\z>x. z < y)" consts RBT_Impl_diag :: "('a, 'b) rbt \ ('a \ 'a, 'b) rbt" class proper_intrvl = ord + fixes proper_interval :: "'a option \ 'a option \ bool" Found termination order: "{}" ### Missing patterns in function definition: ### rbt_keys_next ([], rbt.Empty) = undefined Found termination order: "(\p. size (snd p)) <*mlex*> {}" ### Missing patterns in function definition: ### rbt_entries_next ([], rbt.Empty) = undefined Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. length (snd (snd p))) <*mlex*> (\p. length (fst (snd p))) <*mlex*> {}" ### theory "Containers.RBT_ext" ### 2.587s elapsed time, 5.084s cpu time, 0.704s GC time Loading theory "Regular-Sets.Regular_Set" (required by "Containers.Compatibility_Containers_Regular_Sets" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking" via "Regular-Sets.NDerivative" via "Regular-Sets.Regular_Exp") Found termination order: "(\p. length (snd (snd p))) <*mlex*> (\p. length (fst (snd p))) <*mlex*> {}" class proper_intrvl = ord + fixes proper_interval :: "'a option \ 'a option \ bool" Found termination order: "(\p. length (snd p)) <*mlex*> {}" Found termination order: "{}" datatype 'a ref = ref of 'a ROOT.ML:16: warning: Value identifier (A_) has not been referenced. ROOT.ML:13: warning: Value identifier (x22) has not been referenced. ROOT.ML:13: warning: Value identifier (x21) has not been referenced. ROOT.ML:13: warning: Value identifier (A_) has not been referenced. ROOT.ML:12: warning: Value identifier (x22) has not been referenced. ROOT.ML:12: warning: Value identifier (x21) has not been referenced. ROOT.ML:12: warning: Value identifier (A_) has not been referenced. ROOT.ML:23: warning: Value identifier (f) has not been referenced. ROOT.ML:25: warning: Value identifier (f) has not been referenced. ROOT.ML:28: warning: Value identifier (f) has not been referenced. ROOT.ML:31: warning: Matches are not exhaustive. Found near fun image f (... ...) = Set (... ... xs) ROOT.ML:33: warning: Value identifier (y) has not been referenced. ROOT.ML:33: warning: Value identifier (A_) has not been referenced. ROOT.ML:39: warning: Value identifier (x) has not been referenced. ROOT.ML:39: warning: Value identifier (A_) has not been referenced. ROOT.ML:48: warning: Value identifier (p) has not been referenced. ROOT.ML:56: warning: Matches are not exhaustive. Found near fun product (Set xs) (... ...) = Set (... ... xs) structure Generated_Code: sig val conc: 'a equal -> 'a list set -> 'a list set -> 'a list set type 'a equal type 'a set end overloading lang_pow \ compow :: nat \ 'a list set \ 'a list set consts lang_pow :: "nat \ 'a list set \ 'a list set" ### theory "Regular-Sets.Regular_Set" ### 3.546s elapsed time, 4.344s cpu time, 0.592s GC time Loading theory "Regular-Sets.Regular_Exp" (required by "Containers.Compatibility_Containers_Regular_Sets" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking" via "Regular-Sets.NDerivative") Found termination order: "(\p. length (snd p)) <*mlex*> {}" Found termination order: "(\p. length (snd (snd (snd p)))) <*mlex*> (\p. length (fst (snd (snd p)))) <*mlex*> {}" consts lang :: "'a rexp \ 'a list set" consts nullable :: "'a rexp \ bool" consts rexp_empty :: "'a rexp \ bool" instantiation rexp :: (order) order less_eq_rexp == less_eq :: 'a rexp \ 'a rexp \ bool less_rexp == less :: 'a rexp \ 'a rexp \ bool Found termination order: "(\p. length (snd (snd p))) <*mlex*> (\p. length (fst (snd p))) <*mlex*> {}" instantiation unit :: proper_interval proper_interval_unit == proper_interval :: unit option \ unit option \ bool Found termination order: "{}" instantiation bool :: proper_interval proper_interval_bool == proper_interval :: bool option \ bool option \ bool Found termination order: "{}" instantiation nat :: proper_interval proper_interval_nat == proper_interval :: nat option \ nat option \ bool Found termination order: "{}" instantiation int :: proper_interval proper_interval_int == proper_interval :: int option \ int option \ bool Found termination order: "{}" instantiation integer :: proper_interval proper_interval_integer == proper_interval :: integer option \ integer option \ bool instantiation natural :: proper_interval proper_interval_natural == proper_interval :: natural option \ natural option \ bool instantiation char :: proper_interval proper_interval_char == proper_interval :: char option \ char option \ bool Found termination order: "{}" instantiation Enum.finite_1 :: proper_interval proper_interval_finite_1 == proper_interval :: Enum.finite_1 option \ Enum.finite_1 option \ bool instantiation Enum.finite_2 :: proper_interval proper_interval_finite_2 == proper_interval :: Enum.finite_2 option \ Enum.finite_2 option \ bool Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "{}" instantiation Enum.finite_3 :: proper_interval proper_interval_finite_3 == proper_interval :: Enum.finite_3 option \ Enum.finite_3 option \ bool instantiation rexp :: (linorder) linorder ### theory "Regular-Sets.Regular_Exp" ### 3.575s elapsed time, 7.124s cpu time, 0.584s GC time Loading theory "Regular-Sets.NDerivative" (required by "Containers.Compatibility_Containers_Regular_Sets" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking") Found termination order: "{}" class proper_intrvl = ord + fixes proper_interval :: "'a option \ 'a option \ bool" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" ### theory "Containers.Set_Linorder" ### 12.102s elapsed time, 21.288s cpu time, 2.296s GC time Loading theory "Containers.Collection_Order" class ccompare = type + fixes ccompare :: "('a \ 'a \ order) option" assumes "ccompare": "\comp. ccompare = Some comp \ comparator comp" class ccompare = type + fixes ccompare :: "('a \ 'a \ order) option" assumes "ccompare": "\comp. ccompare = Some comp \ comparator comp" signature CCOMPARE_GENERATOR = sig val ccompare_instance_via_comparator: string -> theory -> theory val ccompare_instance_via_compare: string -> theory -> theory val derive_no_ccompare: string -> theory -> theory end structure CCompare_Generator: CCOMPARE_GENERATOR deriving "compare_order" instance for type "Enum.finite_1" deriving "compare" instance for type "Enum.finite_1" deriving "compare_order" instance for type "Enum.finite_2" deriving "compare" instance for type "Enum.finite_2" deriving "compare_order" instance for type "Enum.finite_3" deriving "compare" instance for type "Enum.finite_3" deriving "compare_order" instance for type "Code_Numeral.natural" deriving "compare" instance for type "Code_Numeral.natural" deriving "compare_order" instance for type "String.literal" deriving "compare" instance for type "String.literal" deriving "ccompare_order" instance for type "Product_Type.unit" via compare_order derived is_ccompare_unit-lemma deriving "ccompare_order" instance for type "HOL.bool" via compare_order derived is_ccompare_bool-lemma deriving "ccompare_order" instance for type "Nat.nat" via compare_order derived is_ccompare_nat-lemma deriving "ccompare_order" instance for type "Int.int" via compare_order derived is_ccompare_int-lemma deriving "ccompare_order" instance for type "Enum.finite_1" via compare_order derived is_ccompare_finite_1-lemma deriving "ccompare_order" instance for type "Enum.finite_2" via compare_order derived is_ccompare_finite_2-lemma deriving "ccompare_order" instance for type "Enum.finite_3" via compare_order derived is_ccompare_finite_3-lemma deriving "ccompare_order" instance for type "Code_Numeral.integer" via compare_order derived is_ccompare_integer-lemma deriving "ccompare_order" instance for type "Code_Numeral.natural" via compare_order derived is_ccompare_natural-lemma deriving "ccompare_order" instance for type "String.char" via compare_order derived is_ccompare_char-lemma deriving "ccompare_order" instance for type "String.literal" via compare_order derived is_ccompare_literal-lemma use None as trivial implementation of ccompare for type finite_4 registered finite_4 in class ccompare use None as trivial implementation of ccompare for type finite_5 registered finite_5 in class ccompare deriving "ccompare" instance for type "Sum_Type.sum" derived is_ccompare_sum-lemma deriving "ccompare" instance for type "List.list" derived is_ccompare_list-lemma deriving "ccompare" instance for type "Option.option" derived is_ccompare_option-lemma deriving "ccompare" instance for type "Product_Type.prod" derived is_ccompare_prod-lemma use None as trivial implementation of ccompare for type fun registered fun in class ccompare instantiation set :: (ccompare) ccompare ccompare_set == ccompare :: ('a set \ 'a set \ order) option use None as trivial implementation of ccompare for type pred registered pred in class ccompare class cproper_interval = ccompare + fixes cproper_interval :: "'a option \ 'a option \ bool" assumes "cproper_interval": "\ID ccompare \ None; finite UNIV\ \ class.proper_interval cless cproper_interval" instantiation unit :: cproper_interval cproper_interval_unit == cproper_interval :: unit option \ unit option \ bool instantiation bool :: cproper_interval cproper_interval_bool == cproper_interval :: bool option \ bool option \ bool instantiation nat :: cproper_interval cproper_interval_nat == cproper_interval :: nat option \ nat option \ bool instantiation int :: cproper_interval cproper_interval_int == cproper_interval :: int option \ int option \ bool instantiation integer :: cproper_interval cproper_interval_integer == cproper_interval :: integer option \ integer option \ bool instantiation natural :: cproper_interval cproper_interval_natural == cproper_interval :: natural option \ natural option \ bool instantiation char :: cproper_interval cproper_interval_char == cproper_interval :: char option \ char option \ bool instantiation Enum.finite_1 :: cproper_interval cproper_interval_finite_1 == cproper_interval :: Enum.finite_1 option \ Enum.finite_1 option \ bool instantiation Enum.finite_2 :: cproper_interval cproper_interval_finite_2 == cproper_interval :: Enum.finite_2 option \ Enum.finite_2 option \ bool instantiation Enum.finite_3 :: cproper_interval cproper_interval_finite_3 == cproper_interval :: Enum.finite_3 option \ Enum.finite_3 option \ bool Found termination order: "(\p. size (fst p)) <*mlex*> (\p. size (snd p)) <*mlex*> {}" instantiation Enum.finite_4 :: cproper_interval cproper_interval_finite_4 == cproper_interval :: Enum.finite_4 option \ Enum.finite_4 option \ bool instantiation Enum.finite_5 :: cproper_interval cproper_interval_finite_5 == cproper_interval :: Enum.finite_5 option \ Enum.finite_5 option \ bool instantiation sum :: (cproper_interval, cproper_interval) cproper_interval cproper_interval_sum == cproper_interval :: ('a + 'b) option \ ('a + 'b) option \ bool Found termination order: "{}" instantiation prod :: (cproper_interval, cproper_interval) cproper_interval cproper_interval_prod == cproper_interval :: ('a \ 'b) option \ ('a \ 'b) option \ bool Found termination order: "{}" instantiation list :: (ccompare) cproper_interval cproper_interval_list == cproper_interval :: 'a list option \ 'a list option \ bool instantiation String.literal :: cproper_interval cproper_interval_literal == cproper_interval :: String.literal option \ String.literal option \ bool instantiation option :: (cproper_interval) cproper_interval cproper_interval_option == cproper_interval :: 'a option option \ 'a option option \ bool Found termination order: "{}" instantiation set :: (cproper_interval) cproper_interval cproper_interval_set == cproper_interval :: 'a set option \ 'a set option \ bool ### Not an equation, in theorem: ### cproper_interval_set_dom (None, None) \ ### cproper_interval None None \ True ### Not an equation, in theorem: ### cproper_interval_set_dom (None, Some ?B) \ ### cproper_interval None (Some ?B) \ ?B \ {} ### Not an equation, in theorem: ### cproper_interval_set_dom (Some ?A, None) \ ### cproper_interval (Some ?A) None \ ?A \ UNIV ### Not an equation, in theorem: ### cproper_interval_set_dom (Some ?A, Some ?B) \ ### cproper_interval (Some ?A) (Some ?B) \ ### finite UNIV \ (\C. cless ?A C \ cless C ?B) Found termination order: "{}" instantiation fun :: (type, type) cproper_interval cproper_interval_fun == cproper_interval :: ('a \ 'b) option \ ('a \ 'b) option \ bool ### theory "Containers.Collection_Order" ### 3.580s elapsed time, 7.368s cpu time, 3.384s GC time Loading theory "Containers.List_Proper_Interval" instantiation list :: ({order,proper_interval}) proper_interval proper_interval_list == proper_interval :: 'a list option \ 'a list option \ bool Found termination order: "{}" ### theory "Containers.List_Proper_Interval" ### 0.545s elapsed time, 1.088s cpu time, 0.000s GC time Loading theory "Containers.RBT_Mapping2" (required by "Containers.Containers" via "Containers.Mapping_Impl") Found termination order: "(\p. size (fst p)) <*mlex*> {}" consts norm :: "'a rexp \ 'a rexp" consts nderiv :: "'a \ 'a rexp \ 'a rexp" ### theory "Regular-Sets.NDerivative" ### 5.968s elapsed time, 12.096s cpu time, 3.800s GC time Loading theory "Regular-Sets.Equivalence_Checking" (required by "Containers.Compatibility_Containers_Regular_Sets" via "Regular-Sets.Regexp_Method") Proofs for coinductive predicate(s) "bisimilar" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... consts add_atoms :: "'a rexp \ 'a list \ 'a list" ### theory "Regular-Sets.Equivalence_Checking" ### 0.395s elapsed time, 0.788s cpu time, 0.000s GC time Loading theory "Regular-Sets.Relation_Interpretation" (required by "Containers.Compatibility_Containers_Regular_Sets" via "Regular-Sets.Regexp_Method") consts rel :: "('a \ ('b \ 'b) set) \ 'a rexp \ ('b \ 'b) set" consts word_rel :: "('a \ ('b \ 'b) set) \ 'a list \ ('b \ 'b) set" ### theory "Regular-Sets.Relation_Interpretation" ### 0.097s elapsed time, 0.192s cpu time, 0.000s GC time Loading theory "Regular-Sets.Regexp_Method" (required by "Containers.Compatibility_Containers_Regular_Sets") consts rel_of_regexp :: "('a \ 'a) set list \ nat rexp \ ('a \ 'a) set" consts rel_eq :: "nat rexp \ nat rexp \ ('a \ 'a) set list \ bool" ### Ambiguous input (line 247 of "~~/afp/thys/Containers/RBT_Mapping2.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" lookup) ### ("_applC" ("_position" meet) ### ("_cargs" ("_position" f) ### ("_cargs" ### ("_constrain" ("_position" t1) ### ("_tappl" ("_position_sort" 'a) ("_position_sort" 'b) ### ("_type_name" mapping_rbt))) ### ("_position" t2))))) ### ("_lambda" ("_position" k) ### ("_case_syntax" ### ("_applC" ("_position" lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ("_applC" ("_position" Some) ("_position" v1)) ### ("_case_syntax" ### ("_applC" ("_position" lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case1" ("_applC" ("_position" Some) ("_position" v2)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v1) ### ("_position" v2)))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" lookup) ### ("_applC" ("_position" meet) ### ("_cargs" ("_position" f) ### ("_cargs" ### ("_constrain" ("_position" t1) ### ("_tappl" ("_position_sort" 'a) ("_position_sort" 'b) ### ("_type_name" mapping_rbt))) ### ("_position" t2))))) ### ("_lambda" ("_position" k) ### ("_case_syntax" ### ("_applC" ("_position" lookup) ### ("_cargs" ("_position" t1) ("_position" k))) ### ("_case2" ("_case1" ("_position" None) ("_position" None)) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" v1)) ### ("_case_syntax" ### ("_applC" ("_position" lookup) ### ("_cargs" ("_position" t2) ("_position" k))) ### ("_case1" ("_position" None) ("_position" None)))) ### ("_case1" ("_applC" ("_position" Some) ("_position" v2)) ### ("_applC" ("_position" Some) ### ("_applC" ("_position" f) ### ("_cargs" ("_position" k) ### ("_cargs" ("_position" v1) ("_position" v2)))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Containers.RBT_Mapping2" ### 1.807s elapsed time, 3.572s cpu time, 0.308s GC time Loading theory "Containers.RBT_Set2" (required by "Containers.Containers" via "Containers.Mapping_Impl" via "Containers.Set_Impl") val regexp_conv = fn: Proof.context -> conv ### theory "Regular-Sets.Regexp_Method" ### 1.075s elapsed time, 2.108s cpu time, 0.308s GC time class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "Containers.RBT_Set2" ### 1.697s elapsed time, 3.396s cpu time, 0.000s GC time Loading theory "Containers.Set_Impl" (required by "Containers.Containers" via "Containers.Mapping_Impl") ### Introduced fixed type variable(s): 'b in "xs__" Found termination order: "size <*mlex*> {}" ### Introduced fixed type variable(s): 'c, 'd, 'e, 'f in "has_next1__" or "has_next2__" or "next1__" or "next2__" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g Found termination order: "length <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" structure Set_Complement_Eqs: NAMED_THMS ### Code generator: dropping subsumed code equation ### Collect ?P \ set (filter ?P enum_class.enum) ### Ambiguous input (line 746 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.union" ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union RBT_set DList_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union RBT_set DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ("_position" RBT_Set2.insert) ### ("_cargs" ("_position" dxs) ### ("_position" rbt))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.union" ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union RBT_set DList_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union RBT_set DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ("_position" RBT_Set2.insert) ### ("_cargs" ("_position" dxs) ("_position" rbt))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 751 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.union" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ("_position" rbt))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union DList_set RBT_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union DList_set RBT_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ("_position" RBT_Set2.insert) ### ("_cargs" ("_position" dxs) ### ("_position" rbt))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.union" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ("_position" rbt))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union DList_set RBT_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''union DList_set RBT_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.union" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ("_position" RBT_Set2.insert) ### ("_cargs" ("_position" dxs) ("_position" rbt))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 830 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.inter" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ("_position" rbt))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter DList_set RBT_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ("_position" rbt))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter DList_set RBT_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" RBT_Set2.inter_list) ### ("_cargs" ("_position" rbt) ### ("_applC" ("_position" list_of_dlist) ### ("_position" dxs))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.inter" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ("_position" rbt))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter DList_set RBT_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ("_position" rbt))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter DList_set RBT_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" RBT_Set2.inter_list) ### ("_cargs" ("_position" rbt) ### ("_applC" ("_position" list_of_dlist) ### ("_position" dxs))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 845 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.inter" ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter RBT_set DList_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter RBT_set DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" RBT_Set2.inter_list) ### ("_cargs" ("_position" rbt) ### ("_applC" ("_position" list_of_dlist) ### ("_position" dxs))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Set.inter" ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter RBT_set DList_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''inter RBT_set DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Set.inter" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" RBT_Set2.inter_list) ### ("_cargs" ("_position" rbt) ### ("_applC" ("_position" list_of_dlist) ### ("_position" dxs))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Code generator: dropping subsumed code equation ### Inf ?A ?x \ INF f:?A. f ?x ### Code generator: dropping subsumed code equation ### Sup ?A ?x \ SUP f:?A. f ?x ### Ambiguous input (line 958 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" csorted_list_of_set) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''csorted_list_of_set DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" csorted_list_of_set) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''csorted_list_of_set DList_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" csorted_list_of_set) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c)) ### ("_applC" ("_position" ord.quicksort) ### ("_cargs" ### ("_applC" ("_position" lt_of_comp) ("_position" c)) ### ("_applC" ("_position" list_of_dlist) ### ("_position" dxs)))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" csorted_list_of_set) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''csorted_list_of_set DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" csorted_list_of_set) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''csorted_list_of_set DList_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" csorted_list_of_set) ### ("_applC" ("_position" DList_set) ### ("_position" dxs))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c)) ### ("_applC" ("_position" ord.quicksort) ### ("_cargs" ("_applC" ("_position" lt_of_comp) ("_position" c)) ### ("_applC" ("_position" list_of_dlist) ### ("_position" dxs)))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Found termination order: "(\p. length (snd (snd p))) <*mlex*> (\p. length (fst (snd p))) <*mlex*> {}" Found termination order: "(\p. length (snd (snd p))) <*mlex*> (\p. length (fst (snd p))) <*mlex*> {}" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" ### Ambiguous input (line 1351 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''the_elem DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" list_of_dlist) ("_position" dxs)) ### ("_case2" ("_case1" ("_list" ("_position" x)) ("_position" x)) ### ("_case1" ("\<^const>Pure.dummy_pattern") ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''the_elem DList_set: not unique'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" DList_set) ### ("_position" dxs)))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" DList_set) ("_position" dxs))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''the_elem DList_set: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" DList_set) ("_position" dxs))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" list_of_dlist) ("_position" dxs)) ### ("_case1" ("_list" ("_position" x)) ("_position" x)))) ### ("_case1" ("\<^const>Pure.dummy_pattern") ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''the_elem DList_set: not unique'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" DList_set) ### ("_position" dxs)))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1356 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" RBT_set) ("_position" rbt))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''the_elem RBT_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" RBT_set) ("_position" rbt))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" RBT_Mapping2.impl_of) ("_position" rbt)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" RBT_Impl.Branch) ### ("_cargs" ("\<^const>Pure.dummy_pattern") ### ("_cargs" ("_position" RBT_Impl.Empty) ### ("_cargs" ("_position" x) ### ("_cargs" ("\<^const>Pure.dummy_pattern") ### ("_position" RBT_Impl.Empty)))))) ### ("_position" x)) ### ("_case1" ("\<^const>Pure.dummy_pattern") ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''the_elem RBT_set: not unique'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt)))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" RBT_set) ("_position" rbt))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''the_elem RBT_set: ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" RBT_set) ("_position" rbt))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" RBT_Mapping2.impl_of) ### ("_position" rbt)) ### ("_case1" ### ("_applC" ("_position" RBT_Impl.Branch) ### ("_cargs" ("\<^const>Pure.dummy_pattern") ### ("_cargs" ("_position" RBT_Impl.Empty) ### ("_cargs" ("_position" x) ### ("_cargs" ("\<^const>Pure.dummy_pattern") ### ("_position" RBT_Impl.Empty)))))) ### ("_position" x)))) ### ("_case1" ("\<^const>Pure.dummy_pattern") ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''the_elem RBT_set: not unique'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" the_elem) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt)))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1412 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" DList_set) ("_position" dys)))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''product DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" DList_set) ### ("_position" dys)))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''product DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" DList_set) ### ("_position" dxs)) ### ("_applC" ("_position" DList_set) ### ("_position" dys)))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_set) ### ("_applC" ("_position" DList_Set.product) ### ("_cargs" ("_position" dxs) ("_position" dys)))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" DList_set) ("_position" dys)))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''product DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_applC" ("_position" DList_set) ### ("_position" dys)))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''product DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" DList_set) ### ("_position" dxs)) ### ("_applC" ("_position" DList_set) ### ("_position" dys)))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_set) ### ("_applC" ("_position" DList_Set.product) ### ("_cargs" ("_position" dxs) ("_position" dys)))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1428 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2)))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''product RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2)))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''product RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2)))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" RBT_Set2.product) ### ("_cargs" ("_position" rbt1) ### ("_position" rbt2)))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2)))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''product RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2)))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''product RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Product_Type.product) ### ("_cargs" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2)))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ### ("_applC" ("_position" RBT_Set2.product) ### ("_cargs" ("_position" rbt1) ("_position" rbt2)))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1495 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.Image" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ("_position" B)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''Image DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_position" B)))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''Image DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_position" B)))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_position" acc)) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" x) ### ("_position" B)) ### ("_applC" ("_position" insert) ### ("_cargs" ("_position" y) ("_position" acc))) ### ("_position" acc))) ### ("_cargs" ("_position" dxs) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.Image" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ("_position" B)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''Image DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_position" B)))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''Image DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" DList_set) ("_position" dxs)) ### ("_position" B)))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_pattern" ("_position" x) ("_position" y)) ### ("_position" acc)) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" x) ("_position" B)) ### ("_applC" ("_position" insert) ### ("_cargs" ("_position" y) ("_position" acc))) ### ("_position" acc))) ### ("_cargs" ("_position" dxs) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1502 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.Image" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ("_position" C)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''Image RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_position" C)))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''Image RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_position" C)))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_position" acc)) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" x) ### ("_position" C)) ### ("_applC" ("_position" insert) ### ("_cargs" ("_position" y) ("_position" acc))) ### ("_position" acc))) ### ("_cargs" ("_position" rbt) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.Image" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ("_position" C)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ("_position" ''Image RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_position" C)))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''Image RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.Image" ### ("_applC" ("_position" RBT_set) ("_position" rbt)) ### ("_position" C)))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_pattern" ("_position" x) ("_position" y)) ### ("_position" acc)) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" x) ("_position" C)) ### ("_applC" ("_position" insert) ### ("_cargs" ("_position" y) ("_position" acc))) ### ("_position" acc))) ### ("_cargs" ("_position" rbt) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1571 of "~~/afp/thys/Containers/Set_Impl.thy") produces 5 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ("_cargs" ("_position" y) ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt2)))) ### ("_cargs" ("_position" rbt1) ### ("\<^const>Set.empty"))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt2)))) ### ("_cargs" ("_position" rbt1) ### ("\<^const>Set.empty"))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt2)))) ### ("_cargs" ("_position" rbt1) ### ("\<^const>Set.empty"))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt2)))) ### ("_cargs" ("_position" rbt1) ### ("\<^const>Set.empty"))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp RBT_set RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ("_position" rbt2))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'c))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt1)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt2)))))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt2)))) ### ("_cargs" ("_position" rbt1) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1580 of "~~/afp/thys/Containers/Set_Impl.thy") produces 14 parse trees (10 displayed): ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ### ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1)))))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty"))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'e))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'e))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'e))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ("_position" dxs1))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1)))))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ### ("_position" rbt3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs1))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs1)))) ### ("_cargs" ("_position" rbt3) ### ("\<^const>Set.empty"))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1591 of "~~/afp/thys/Containers/Set_Impl.thy") produces 14 parse trees (10 displayed): ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ### ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4)))))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty"))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set RBT_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ("_position" rbt4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'd))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'd))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4)))))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set RBT_set: ccompare3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs2)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" rbt4)))) ### ("_cargs" ("_position" dxs2) ### ("\<^const>Set.empty"))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Rule already declared as elimination (elim) ### \?w \ ?A @@ ?B; ### \u v. ### \u \ ?A; v \ ?B; ?w = u @ v\ ### \ ?thesis\ ### \ ?thesis ### Ambiguous input (line 1602 of "~~/afp/thys/Containers/Set_Impl.thy") produces 5 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'g))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ("_tuple" ("_position" x) ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" dxs3) ### ("\<^const>Set.empty"))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'g))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" dxs3) ### ("\<^const>Set.empty"))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'g))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ### ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" dxs3) ### ("\<^const>Set.empty"))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'g))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" dxs3) ### ("\<^const>Set.empty"))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CEQ" ("_position_sort" 'g))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set DList_set: ceq3 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4)))))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" dxs3) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1616 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" Set_Monad) ("_position" xs3))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set Set_Monad: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" Set_Monad) ("_position" xs3))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set Set_Monad: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" Set_Monad) ### ("_position" xs3))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" xs3)))) ### ("_cargs" ("_position" rbt1) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" Set_Monad) ("_position" xs3))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set Set_Monad: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" Set_Monad) ("_position" xs3))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp RBT_set Set_Monad: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" RBT_set) ("_position" rbt1)) ### ("_applC" ("_position" Set_Monad) ### ("_position" xs3))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" xs3)))) ### ("_cargs" ("_position" rbt1) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1623 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs4)) ### ("_applC" ("_position" RBT_set) ("_position" rbt5))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp Set_Monad RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs4)) ### ("_applC" ("_position" RBT_set) ("_position" rbt5))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp Set_Monad RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs4)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt5))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ### ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt5)))) ### ("_cargs" ("_position" xs4) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs4)) ### ("_applC" ("_position" RBT_set) ("_position" rbt5))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp Set_Monad RBT_set: ccompare1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs4)) ### ("_applC" ("_position" RBT_set) ("_position" rbt5))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'b))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp Set_Monad RBT_set: ccompare2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs4)) ### ("_applC" ("_position" RBT_set) ### ("_position" rbt5))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c_b)) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" RBT_Set2.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c_b) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_position" Eq)) ### ("_position" A) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))))) ### ("_position" rbt5)))) ### ("_cargs" ("_position" xs4) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1630 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" Set_Monad) ("_position" xs5))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set Set_Monad: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" Set_Monad) ("_position" xs5))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set Set_Monad: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" Set_Monad) ### ("_position" xs5))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" xs5)))) ### ("_cargs" ("_position" dxs3) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" Set_Monad) ("_position" xs5))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'e))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp DList_set Set_Monad: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ("_position" dxs3)) ### ("_applC" ("_position" Set_Monad) ("_position" xs5))))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp DList_set Set_Monad: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" DList_set) ### ("_position" dxs3)) ### ("_applC" ("_position" Set_Monad) ### ("_position" xs5))))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" xs5)))) ### ("_cargs" ("_position" dxs3) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1637 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs6)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp Set_Monad DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs6)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'g))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp Set_Monad DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs6)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" xs6) ### ("\<^const>Set.empty")))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs6)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'f))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''relcomp Set_Monad DList_set: ceq1 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs6)) ### ("_applC" ("_position" DList_set) ("_position" dxs4))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'g))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''relcomp Set_Monad DList_set: ceq2 = None'')) ### ("_lambda" ("_idtdummy") ### ("\<^const>Relation.relcomp" ### ("_applC" ("_position" Set_Monad) ("_position" xs6)) ### ("_applC" ("_position" DList_set) ### ("_position" dxs4))))))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" fold) ### ("_cargs" ### ("_lambda" ("_pattern" ("_position" x) ("_position" y)) ### ("_applC" ("_position" DList_Set.fold) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ### ("_pattern" ("_position" y') ("_position" z)) ### ("_position" A)) ### ("\<^const>HOL.If" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" y) ("_position" y'))) ### ("_applC" ("_position" insert) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" z))) ### ("_position" A))) ### ("_position" A))) ### ("_position" dxs4)))) ### ("_cargs" ("_position" xs6) ("\<^const>Set.empty")))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1654 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.iff" ("_applC" ("_position" irrefl) ("_position" r)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_Ball" ("_pattern" ("_position" x) ("_position" y)) ### ("_position" r) ### ("\<^const>HOL.Not" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" x) ("_position" y)))))) ### ("_case1" ("_position" None) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''irrefl: ceq = None & ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" irrefl) ("_position" r)))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c)) ### ("_Ball" ("_pattern" ("_position" x) ("_position" y)) ### ("_position" r) ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c) ### ("_cargs" ("_position" x) ("_position" y))) ### ("_position" Eq))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.iff" ("_applC" ("_position" irrefl) ("_position" r)) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_Ball" ("_pattern" ("_position" x) ("_position" y)) ### ("_position" r) ### ("\<^const>HOL.Not" ### ("_applC" ("_position" eq) ### ("_cargs" ("_position" x) ("_position" y)))))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_case_syntax" ### ("_applC" ("_position" ID) ### ("_CCOMPARE" ("_position_sort" 'a))) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ### ''irrefl: ceq = None & ccompare = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" irrefl) ("_position" r)))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c)) ### ("_Ball" ("_pattern" ("_position" x) ("_position" y)) ### ("_position" r) ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" c) ### ("_cargs" ("_position" x) ("_position" y))) ### ("_position" Eq))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1747 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" can_select) ### ("_cargs" ("_position" P) ### ("_applC" ("_position" Set_Monad) ("_position" xs)))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''can_select Set_Monad: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" can_select) ### ("_cargs" ("_position" P) ### ("_applC" ("_position" Set_Monad) ### ("_position" xs)))))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" filter) ### ("_cargs" ("_position" P) ("_position" xs))) ### ("_case2" ("_case1" ("_position" Nil) ("_position" False)) ### ("_case1" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" list_all) ### ("_cargs" ("_applC" ("_position" eq) ("_position" x)) ### ("_position" xs))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" can_select) ### ("_cargs" ("_position" P) ### ("_applC" ("_position" Set_Monad) ("_position" xs)))) ### ("_case_syntax" ### ("_applC" ("_position" ID) ("_CEQ" ("_position_sort" 'a))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Code.abort) ### ("_cargs" ### ("_Literal" ### ("_position" ''can_select Set_Monad: ceq = None'')) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" can_select) ### ("_cargs" ("_position" P) ### ("_applC" ("_position" Set_Monad) ### ("_position" xs)))))))) ### ("_case2" ### ("_case1" ("_applC" ("_position" Some) ("_position" eq)) ### ("_case_syntax" ### ("_applC" ("_position" filter) ### ("_cargs" ("_position" P) ("_position" xs))) ### ("_case1" ("_position" Nil) ("_position" False)))) ### ("_case1" ### ("\<^const>List.list.Cons" ("_position" x) ("_position" xs)) ### ("_applC" ("_position" list_all) ### ("_cargs" ("_applC" ("_position" eq) ("_position" x)) ### ("_position" xs))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 1858 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_constrain" ("_position" set_empty_choose) ### ("_tapp" ### ("_ofsort" ("_position_sort" 'a) ### ("_sort" ### ("_classes" ("_class_name" ceq) ("_class_name" ccompare)))) ### ("_type_name" set))) ### ("_case_syntax" ("_CCOMPARE" ("_position_sort" 'a)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ("_position" RBT_Set2.empty))) ### ("_case1" ("_position" None) ### ("_case_syntax" ("_CEQ" ("_position_sort" 'a)) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" Set_Monad) ### ("\<^const>List.list.Nil"))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_set) ### ("_position" DList_Set.empty)))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_constrain" ("_position" set_empty_choose) ### ("_tapp" ### ("_ofsort" ("_position_sort" 'a) ### ("_sort" ### ("_classes" ("_class_name" ceq) ("_class_name" ccompare)))) ### ("_type_name" set))) ### ("_case_syntax" ("_CCOMPARE" ("_position_sort" 'a)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" RBT_set) ("_position" RBT_Set2.empty))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_case_syntax" ("_CEQ" ("_position_sort" 'a)) ### ("_case1" ("_position" None) ### ("_applC" ("_position" Set_Monad) ### ("\<^const>List.list.Nil"))))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" DList_set) ### ("_position" DList_Set.empty)))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. class set_impl = type + fixes set_impl :: "('a, set_impl) phantom" signature SET_IMPL_GENERATOR = sig val derive_set_impl: string -> string -> theory -> theory end structure Set_Impl_Generator: SET_IMPL_GENERATOR use dlist as set_impl for type unit registered unit in class set_impl use dlist as set_impl for type bool registered bool in class set_impl use rbt as set_impl for type nat registered nat in class set_impl use set_RBT as set_impl for type int registered int in class set_impl use dlist as set_impl for type finite_1 registered finite_1 in class set_impl use dlist as set_impl for type finite_2 registered finite_2 in class set_impl use dlist as set_impl for type finite_3 registered finite_3 in class set_impl use rbt as set_impl for type integer registered integer in class set_impl use rbt as set_impl for type natural registered natural in class set_impl use rbt as set_impl for type char registered char in class set_impl instantiation sum :: (set_impl, set_impl) set_impl set_impl_sum == set_impl :: ('a + 'b, set_impl) phantom instantiation prod :: (set_impl, set_impl) set_impl set_impl_prod == set_impl :: ('a \ 'b, set_impl) phantom use choose as set_impl for type list registered list in class set_impl use rbt as set_impl for type literal registered literal in class set_impl instantiation option :: (set_impl) set_impl set_impl_option == set_impl :: ('a option, set_impl) phantom use monad as set_impl for type fun registered fun in class set_impl use choose as set_impl for type set registered set in class set_impl instantiation phantom :: (type, set_impl) set_impl set_impl_phantom == set_impl :: (('a, 'b) phantom, set_impl) phantom ### Ambiguous input (line 1977 of "~~/afp/thys/Containers/Set_Impl.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" set_aux) ("_position" set_Choose)) ### ("_case_syntax" ### ("_CCOMPARE" ### ("_ofsort" ("_position_sort" 'a) ### ("_sort" ### ("_classes" ("_class_name" ccompare) ("_class_name" ceq))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" conv) ### ("_applC" ("_position" RBT_set) ("_position" RBT_Set2.empty)))) ### ("_case1" ("_position" None) ### ("_case_syntax" ("_CEQ" ("_position_sort" 'a)) ### ("_case2" ("_case1" ("_position" None) ("_position" Set_Monad)) ### ("_case1" ### ("_applC" ("_position" Some) ### ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" conv) ### ("_applC" ("_position" DList_set) ### ("_position" DList_Set.empty))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" set_aux) ("_position" set_Choose)) ### ("_case_syntax" ### ("_CCOMPARE" ### ("_ofsort" ("_position_sort" 'a) ### ("_sort" ### ("_classes" ("_class_name" ccompare) ("_class_name" ceq))))) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" conv) ### ("_applC" ("_position" RBT_set) ("_position" RBT_Set2.empty)))) ### ("_case2" ### ("_case1" ("_position" None) ### ("_case_syntax" ("_CEQ" ("_position_sort" 'a)) ### ("_case1" ("_position" None) ("_position" Set_Monad)))) ### ("_case1" ### ("_applC" ("_position" Some) ("\<^const>Pure.dummy_pattern")) ### ("_applC" ("_position" conv) ### ("_applC" ("_position" DList_set) ### ("_position" DList_Set.empty))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Containers.Set_Impl" ### 17.149s elapsed time, 33.972s cpu time, 2.324s GC time Loading theory "Containers.Mapping_Impl" (required by "Containers.Containers") ### theory "Containers.Mapping_Impl" ### 1.165s elapsed time, 2.300s cpu time, 0.272s GC time ### Ignoring duplicate rewrite rule: ### finite ?y \ set (sorted_list_of_set ?y) \ ?y ### Ignoring duplicate rewrite rule: ### sorted (sorted_list_of_set ?A1) \ True ### Ignoring duplicate rewrite rule: ### distinct (sorted_list_of_set ?A1) \ True isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Containers/outline -o pdf -n outline -t /proof,/ML *** Failed to load theory "Containers.Map_To_Mapping" (unresolved "Containers.Mapping_Impl") *** Failed to load theory "Containers.Containers" (unresolved "Containers.Map_To_Mapping", "Containers.Mapping_Impl") *** Failed to load theory "Containers.Containers_Userguide" (unresolved "Containers.Containers") *** Failed to load theory "Containers.Compatibility_Containers_Regular_Sets" (unresolved "Containers.Containers") *** Type unification failed: Clash of types "_ set" and "_ \ _" *** *** Type error in application: incompatible operand type *** *** Operator: pcr_mapping (=) (=) ===> (=) :: *** ((??'a \ ??'b option) \ ??'c) *** \ ((??'a, ??'b) mapping \ ??'c) \ bool *** Operand: \m. m = {} :: ??'d set \ bool *** *** Coercion Inference: *** *** Local coercion insertion on the operand failed: *** No coercion known for type constructors: "fun" and "set" *** At command "lemma" (line 40 of "~~/afp/thys/Containers/Mapping_Impl.thy")