Loading theory "Featherweight_OCL.UML_Types" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library" via "Featherweight_OCL.UML_Boolean" via "Featherweight_OCL.UML_PropertyProfiles" via "Featherweight_OCL.UML_Logic") ### Missing patterns in function definition: ### \\\ = undefined Found termination order: "{}" ### Ignoring duplicate rewrite rule: ### drop \y\ \ y class UML_Types.bot = type + fixes bot :: "'a" assumes "nonEmpty": "\x. x \ UML_Types.bot_class.bot" class null = UML_Types.bot + fixes null :: "'a" assumes "null_is_valid": "null \ UML_Types.bot_class.bot" instantiation option :: (type) UML_Types.bot bot_option == UML_Types.bot_class.bot :: \'a\\<^sub>\ instantiation option :: (UML_Types.bot) null null_option == null :: \'a\\<^sub>\ instantiation fun :: (type, UML_Types.bot) UML_Types.bot bot_fun == UML_Types.bot_class.bot :: 'a \ 'b instantiation fun :: (type, null) null null_fun == null :: 'a \ 'b class object = type + fixes oid_of :: "'a \ nat" "'\" instantiation option :: (object) object oid_of_option == oid_of :: \'a\\<^sub>\ \ nat ### Ignoring sort constraints in type variables(s): "'\" ### in type abbreviation "val" instantiation Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null, null) UML_Types.bot bot_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e == UML_Types.bot_class.bot :: ('a, 'b) Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null, null) null null_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e == null :: ('a, 'b) Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null) UML_Types.bot bot_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e == UML_Types.bot_class.bot :: 'a Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null) null null_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e == null :: 'a Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null) UML_Types.bot bot_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e == UML_Types.bot_class.bot :: 'a Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null) null null_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e == null :: 'a Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null) UML_Types.bot bot_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e == UML_Types.bot_class.bot :: 'a Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (null) null null_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e == null :: 'a Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e val disp_msg = fn: string -> string -> string -> string val lemma = fn: string -> (string -> 'a option -> ('b -> 'c -> 'c) -> binding * 'd list -> 'e list -> 'f list -> ('g, 'h) Element.stmt -> bool -> 'i -> Proof.state) -> ('i -> 'h) -> (('i -> Proof.context) -> 'j -> 'k) -> 'j -> 'k option val outer_syntax_command = fn: Outer_Syntax.command_keyword -> (('a -> 'b) -> Toplevel.transition -> Toplevel.transition) -> ((local_theory -> Proof.context) -> 'a -> 'b) -> unit ### theory "Featherweight_OCL.UML_Types" ### 1.602s elapsed time, 1.920s cpu time, 0.128s GC time Loading theory "Featherweight_OCL.UML_Logic" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library" via "Featherweight_OCL.UML_Boolean" via "Featherweight_OCL.UML_PropertyProfiles") ### Ambiguous input (line 702 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.All_binder" ("_position" \) ("_position" \)) ### ("_position" P))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" P) ("_position" true)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.All_binder" ("_position" \) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" P)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" P) ("_position" true)))) ### 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 754 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" A))) ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("_position" null)) ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ("_position" A))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" A))) ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" A) ("_position" null))) ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ("_position" A))))))) ### 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/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" A) ("_position" true))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("_position" true)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)))) ### 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 849 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" A) ("_position" false))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ("_position" A))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("_position" false)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ("_position" A))))) ### 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 853 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" A) ("_position" invalid))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.valid" ("_position" A)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("_position" invalid)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.valid" ("_position" A)))))) ### 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 860 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X))) ### ("\<^const>HOL.conj" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" X) ("_position" \)) ("_position" bot)) ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" X) ("_position" \)) ### ("_position" null))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>HOL.eq" ("\<^const>UML_Logic.defined" ("_position" X)) ### ("\<^const>HOL.conj" ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" X) ("_position" \)) ("_position" bot)) ### ("\<^const>HOL.not_equal" ### ("_applC" ("_position" X) ("_position" \)) ### ("_position" null)))))) ### 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 923 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.OclImplies" ("_position" A) ("_position" B))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" B))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclImplies" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" A)) ### ("_position" B)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" B))))) ### 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 989 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" y)) ### ("_position" x))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" P))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" P) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" P) ("_position" y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" y) ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" P))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" P) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" P) ("_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. ### Ignoring duplicate safe introduction (intro!) ### cp (\_. c) ### Ignoring duplicate rewrite rule: ### cp (\_. c1) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\X. X) ### Ignoring duplicate rewrite rule: ### cp (\X. X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. not (P X)) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. not (P1 X)) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X and Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X and Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X or Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X or Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X implies Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X implies Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X \ Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X \ Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\_. c) ### Ignoring duplicate rewrite rule: ### cp (\_. c1) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\X. X) ### Ignoring duplicate rewrite rule: ### cp (\X. X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. not (P X)) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. not (P1 X)) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X and Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X and Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X or Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X or Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X implies Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X implies Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X \ Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X \ Q1 X) \ True ### Ambiguous input (line 1109 of "~~/afp/thys/Featherweight_OCL/UML_Logic.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" P))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.OclIf" ("_position" P) ("_position" B\<^sub>1) ### ("_position" B\<^sub>2))) ### ("_position" B\<^sub>1)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" P))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclIf" ("_position" P) ("_position" B\<^sub>1) ### ("_position" B\<^sub>2)) ### ("_position" B\<^sub>1))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Featherweight_OCL.UML_Logic" ### 1.084s elapsed time, 2.028s cpu time, 0.000s GC time Loading theory "Featherweight_OCL.UML_PropertyProfiles" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library" via "Featherweight_OCL.UML_Boolean") locale profile_mono_scheme_defined fixes f :: "('\ state \ '\ state \ '\) \ '\ state \ '\ state \ '\" and g :: "'\ \ '\" assumes "profile_mono_scheme_defined f g" locale profile_mono_schemeV fixes f :: "('\ state \ '\ state \ '\) \ '\ state \ '\ state \ '\" and g :: "'\ \ '\" assumes "profile_mono_schemeV f g" locale profile_mono\<^sub>d fixes f :: "('a state \ 'a state \ 'b) \ 'a state \ 'a state \ 'c" and g :: "'b \ 'c" assumes "profile_mono\<^sub>d f g" locale profile_mono0 fixes f :: "('a state \ 'a state \ 'b) \ 'a state \ 'a state \ 'c" and g :: "'b \ 'c" assumes "profile_mono0 f g" locale profile_mono0 fixes f :: "('a state \ 'a state \ 'b) \ 'a state \ 'a state \ 'c" and g :: "'b \ 'c" assumes "profile_mono0 f g" locale profile_single fixes d :: "('\ state \ '\ state \ 'a) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\" assumes "profile_single d" locale profile_bin_scheme fixes d\<^sub>x :: "('\ state \ '\ state \ 'a) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\" and d\<^sub>y :: "('\ state \ '\ state \ 'b) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\" and f :: "('\ state \ '\ state \ 'a) \ ('\ state \ '\ state \ 'b) \ '\ state \ '\ state \ 'c" and g :: "'a \ 'b \ 'c" assumes "profile_bin_scheme d\<^sub>x d\<^sub>y f g" ### Ambiguous input (line 241 of "~~/afp/thys/Featherweight_OCL/UML_PropertyProfiles.thy") produces 4 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ("_applC" ("_position" f) ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" invalid))) ### ("_position" invalid))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" Y))))) ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ("_applC" ("_position" f) ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" invalid))) ### ("_position" invalid))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" Y))))) ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ("_applC" ("_position" f) ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" invalid))) ### ("_position" invalid))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" Y)))) ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ("_applC" ("_position" f) ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" invalid))) ### ("_position" invalid))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" d\<^sub>y) ("_position" Y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" f) ### ("_cargs" ("_position" X) ("_position" Y)))) ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_applC" ("_position" d\<^sub>y) ("_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. locale profile_bin_scheme_defined fixes d\<^sub>y :: "('\ state \ '\ state \ 'b) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\" and f :: "('\ state \ '\ state \ 'a) \ ('\ state \ '\ state \ 'b) \ '\ state \ '\ state \ 'c" and g :: "'a \ 'b \ 'c" assumes "profile_bin_scheme_defined d\<^sub>y f g" locale profile_bin\<^sub>d_\<^sub>d fixes f :: "('\ state \ '\ state \ 'a) \ ('\ state \ '\ state \ 'b) \ '\ state \ '\ state \ 'c" and g :: "'a \ 'b \ 'c" assumes "profile_bin\<^sub>d_\<^sub>d f g" locale profile_bin\<^sub>d_\<^sub>v fixes f :: "('\ state \ '\ state \ 'a) \ ('\ state \ '\ state \ 'b) \ '\ state \ '\ state \ 'c" and g :: "'a \ 'b \ 'c" assumes "profile_bin\<^sub>d_\<^sub>v f g" locale profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v fixes f :: "('\ state \ '\ state \ '\) \ ('\ state \ '\ state \ '\) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\" assumes "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v f" locale profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v fixes f :: "('\ state \ '\ state \ '\) \ ('\ state \ '\ state \ '\) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\" assumes "profile_bin\<^sub>S\<^sub>t\<^sub>r\<^sub>o\<^sub>n\<^sub>g\<^sub>E\<^sub>q_\<^sub>v_\<^sub>v f" locale profile_bin\<^sub>v_\<^sub>v fixes f :: "('\ state \ '\ state \ '\) \ ('\ state \ '\ state \ '\) \ '\ state \ '\ state \ '\" and g :: "'\ \ '\ \ '\" assumes "profile_bin\<^sub>v_\<^sub>v f g" ### theory "Featherweight_OCL.UML_PropertyProfiles" ### 0.569s elapsed time, 1.136s cpu time, 0.000s GC time Loading theory "Featherweight_OCL.UML_Boolean" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\) \ ('\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### theory "Featherweight_OCL.UML_Boolean" ### 2.348s elapsed time, 4.668s cpu time, 0.372s GC time Loading theory "Featherweight_OCL.UML_Integer" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ \\int\\<^sub>\\\<^sub>\) \ ('\ state \ '\ state \ \\int\\<^sub>\\\<^sub>\) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 261 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Integer.thy") produces 2 parse trees: ### ("notequal" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Integer.OclInt1")) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("notequal" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### 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 262 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Integer.thy") produces 2 parse trees: ### ("notequal" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("notequal" ("\<^const>UML_Integer.OclInt2") ### ("\<^const>UML_Integer.OclInt1"))) ### 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 263 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Integer.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ("\<^const>UML_Integer.OclInt2") ### ("\<^const>UML_Integer.OclInt2"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Featherweight_OCL.UML_Integer" ### 7.789s elapsed time, 15.424s cpu time, 0.388s GC time Loading theory "Featherweight_OCL.UML_Sequence" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ Sequence('\)) \ ('\ state \ '\ state \ Sequence('\)) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 474 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Sequence.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_OclIterateSeq" ### ("\<^const>UML_Sequence.OclIncluding" ("_position" S) ("_position" a)) ### ("_position" b) ("_position" x) ("_position" A) ### ("_applC" ("_position" P) ("_cargs" ("_position" b) ("_position" x)))) ### ("_OclIterateSeq" ("_position" S) ("_position" b) ("_position" x) ### ("_applC" ("_position" P) ("_cargs" ("_position" a) ("_position" A))) ### ("_applC" ("_position" P) ### ("_cargs" ("_position" b) ("_position" x)))))) ### ("\<^const>HOL.Trueprop" ### ("_OclIterateSeq" ### ("\<^const>HOL.eq" ### ("_OclIterateSeq" ### ("\<^const>UML_Sequence.OclIncluding" ("_position" S) ### ("_position" a)) ### ("_position" b) ("_position" x) ("_position" A) ### ("_applC" ("_position" P) ### ("_cargs" ("_position" b) ("_position" x)))) ### ("_position" S)) ### ("_position" b) ("_position" x) ### ("_applC" ("_position" P) ("_cargs" ("_position" a) ("_position" A))) ### ("_applC" ("_position" P) ("_cargs" ("_position" b) ("_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. instantiation Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (equal) equal equal_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e == equal_class.equal :: Sequence('a) \ Sequence('a) \ bool ### Ambiguous input (line 560 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Sequence.thy") produces 3 parse trees: ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinsequence" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.mtSequence") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Integer.OclInt1"))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinsequence" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.mtSequence") ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1")))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinsequence" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Sequence.mtSequence")) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b list\\<^sub>\\\<^sub>\ ### \ \\'b list\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'm::{} not of sort type ### KO: 'nbe' failed to normalize ### Ambiguous input (line 560 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Sequence.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinsequence" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.mtSequence") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Integer.OclInt1")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinsequence" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.mtSequence") ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Sequence.OclPrepend" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinsequence" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Sequence.mtSequence")) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1")))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b list\\<^sub>\\\<^sub>\ ### \ \\'b list\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ak::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\\\'b\\<^sub>\\\<^sub>\ list\\<^sub>\\\<^sub>\ ### \ \\\\'b\\<^sub>\\\<^sub>\ list\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'aw::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### theory "Featherweight_OCL.UML_Sequence" ### 2.795s elapsed time, 5.568s cpu time, 0.160s GC time Loading theory "Featherweight_OCL.UML_Pair" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ Pair('\,'\)) \ ('\ state \ '\ state \ Pair('\,'\)) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 147 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 3 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" Y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Pair.OclPair" ("_position" X) ("_position" Y)))) ### ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" Y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Pair.OclPair" ("_position" X) ("_position" Y))) ### ("_position" X))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" Y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclPair" ("_position" X) ("_position" Y)))) ### ("_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. ### Ambiguous input (line 156 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 3 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Pair.OclPair" ("_position" X) ("_position" Y)))) ### ("_position" Y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Pair.OclPair" ("_position" X) ("_position" Y))) ### ("_position" Y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclPair" ("_position" X) ("_position" Y)))) ### ("_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 Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (equal, equal) equal equal_Pair\<^sub>b\<^sub>a\<^sub>s\<^sub>e == equal_class.equal :: Pair('a,'b) \ Pair('a,'b) \ bool ### Ambiguous input (line 204 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 3 parse trees: ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclFirst" ("_position" invalid))) ### ("_position" invalid)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ("_position" invalid)) ### ("_position" invalid))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" invalid))) ### ("_position" invalid)) ### 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 205 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 3 parse trees: ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclFirst" ("_position" null))) ### ("_position" invalid)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ("_position" null)) ### ("_position" invalid))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" null))) ### ("_position" invalid)) ### 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 206 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 7 parse trees: ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" null))) ### ("_position" invalid))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ("_position" null)) ### ("_position" invalid)))) ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ("_position" null)) ### ("_position" invalid)))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclSecond" ("_position" null))) ### ("\<^const>UML_Pair.OclSecond" ("_position" invalid))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ("_position" null)) ### ("\<^const>UML_Pair.OclSecond" ("_position" invalid)))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" null))) ### ("\<^const>UML_Pair.OclSecond" ("_position" invalid))) ### ("\<^const>UML_Pair.OclSecond" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclSecond" ("_position" null))) ### ("_position" invalid))) ### 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 207 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclPair" ("_position" invalid) ("_position" true))) ### ("_position" invalid)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclPair" ("_position" invalid) ("_position" true)) ### ("_position" invalid))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Type unification failed: Variable ?'a::{} not of sort equal ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: 'a \ 'a \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable ?'a::{} not of sort equal ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### sort mismatch ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Ambiguous input (line 209 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 3 parse trees: ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Pair.OclPair" ("_position" null) ("_position" true)))) ### ("_position" null)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Pair.OclPair" ("_position" null) ("_position" true))) ### ("_position" null))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclPair" ("_position" null) ("_position" true)))) ### ("_position" null)) ### 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 210 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Pair.thy") produces 3 parse trees: ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Pair.OclPair" ("_position" null) ### ("\<^const>UML_Pair.OclPair" ("_position" true) ### ("_position" invalid))))) ### ("_position" invalid)) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Pair.OclPair" ("_position" null) ### ("\<^const>UML_Pair.OclPair" ("_position" true) ### ("_position" invalid)))) ### ("_position" invalid))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Pair.OclFirst" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Pair.OclPair" ("_position" null) ### ("\<^const>UML_Pair.OclPair" ("_position" true) ### ("_position" invalid))))) ### ("_position" invalid)) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Featherweight_OCL.UML_Pair" ### 0.998s elapsed time, 1.996s cpu time, 0.000s GC time Loading theory "Featherweight_OCL.UML_Real" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ \\real\\<^sub>\\\<^sub>\) \ ('\ state \ '\ state \ \\real\\<^sub>\\\<^sub>\) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 260 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Real.thy") produces 2 parse trees: ### ("notequal" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Real.OclReal1")) ### ("\<^const>UML_Real.OclReal2")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("notequal" ("\<^const>UML_Real.OclReal1") ### ("\<^const>UML_Real.OclReal2"))) ### 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 261 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Real.thy") produces 2 parse trees: ### ("notequal" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Real.OclReal2")) ### ("\<^const>UML_Real.OclReal1")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("notequal" ("\<^const>UML_Real.OclReal2") ### ("\<^const>UML_Real.OclReal1"))) ### 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 262 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Real.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Real.OclReal2")) ### ("\<^const>UML_Real.OclReal2")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ("\<^const>UML_Real.OclReal2") ### ("\<^const>UML_Real.OclReal2"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Featherweight_OCL.UML_Real" ### 8.447s elapsed time, 16.776s cpu time, 0.368s GC time Loading theory "Featherweight_OCL.UML_String" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ \\char list\\<^sub>\\\<^sub>\) \ ('\ state \ '\ state \ \\char list\\<^sub>\\\<^sub>\) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 140 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_String.thy") produces 2 parse trees: ### ("notequal" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_String.OclStringa")) ### ("\<^const>UML_String.OclStringb")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("notequal" ("\<^const>UML_String.OclStringa") ### ("\<^const>UML_String.OclStringb"))) ### 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 141 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_String.thy") produces 2 parse trees: ### ("notequal" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_String.OclStringb")) ### ("\<^const>UML_String.OclStringa")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("notequal" ("\<^const>UML_String.OclStringb") ### ("\<^const>UML_String.OclStringa"))) ### 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 142 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_String.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_String.OclStringb")) ### ("\<^const>UML_String.OclStringb")) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ("\<^const>UML_String.OclStringb") ### ("\<^const>UML_String.OclStringb"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "Featherweight_OCL.UML_String" ### 3.496s elapsed time, 6.956s cpu time, 0.112s GC time Loading theory "Featherweight_OCL.UML_Void" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") instantiation Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: UML_Types.bot bot_Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e == UML_Types.bot_class.bot :: Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e instantiation Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: null null_Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e == null :: Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) \ ('\ state \ '\ state \ Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Wellsortedness error: ### Type Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e not of sort {equal,null} ### No type arity Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: equal KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### theory "Featherweight_OCL.UML_Void" ### 0.236s elapsed time, 0.476s cpu time, 0.000s GC time Loading theory "Featherweight_OCL.UML_Bag" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") ### Ambiguous input (line 134 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 10 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ Bag('\)) \ ('\ state \ '\ state \ Bag('\)) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 698 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclSize" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclSize" ("_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. ### Ambiguous input (line 732 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclIsEmpty" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclIsEmpty" ("_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. ### Ambiguous input (line 750 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclNotEmpty" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclNotEmpty" ("_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. ### Ambiguous input (line 755 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.OclNotEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" e) ### ("\<^const>Set.member" ("_position" e) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.OclNotEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" e) ### ("\<^const>Set.member" ("_position" e) ### ("_applC" ("_position" Rep_Bag_base) ### ("_cargs" ("_position" X) ("_position" \)))))))) ### 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 776 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.OclNotEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" e) ### ("\<^const>Set.member" ("_position" e) ### ("_applC" ("_position" Rep_Set_base) ### ("_cargs" ("_position" X) ("_position" \)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.OclNotEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" e) ### ("\<^const>Set.member" ("_position" e) ### ("_applC" ("_position" Rep_Set_base) ### ("_cargs" ("_position" X) ("_position" \)))))))) ### 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 789 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 4 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.OclIsEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclANY" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.OclIsEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclANY" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.OclIsEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclANY" ("_position" X)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.OclIsEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Bag.OclANY" ("_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. ### Ambiguous input (line 975 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_lambda" ### ("_pttrns" ("_position" X) ### ("_pttrns" ("_position" St) ("_position" x))) ### ("_applC" ("_position" P) ### ("_cargs" ("_lambda" ("_position" \) ("_position" x)) ### ("_cargs" ("_position" X) ("_position" St))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" S))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_OclForallBag" ### ("_lambda" ("_position" X) ### ("_applC" ("_position" S) ("_position" X))) ### x ("_applC" ("_position" P) ### ("_cargs" ("_position" x) ("_position" X)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_lambda" ### ("_pttrns" ("_position" X) ### ("_pttrns" ("_position" St) ("_position" x))) ### ("_applC" ("_position" P) ### ("_cargs" ("_lambda" ("_position" \) ("_position" x)) ### ("_cargs" ("_position" X) ("_position" St))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" S))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_lambda" ("_position" X) ### ("_OclForallBag" ("_applC" ("_position" S) ("_position" X)) x ### ("_applC" ("_position" P) ### ("_cargs" ("_position" x) ("_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. instantiation Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (equal) equal equal_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e == equal_class.equal :: Bag('a) \ Bag('a) \ bool ### theory "Featherweight_OCL.UML_Bag" ### 2.432s elapsed time, 4.836s cpu time, 0.136s GC time Loading theory "Featherweight_OCL.UML_Set" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State" via "Featherweight_OCL.UML_Library") ### Ambiguous input (line 126 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 10 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. overloading StrictRefEq \ StrictRefEq :: ('\ state \ '\ state \ Set('\)) \ ('\ state \ '\ state \ Set('\)) \ '\ state \ '\ state \ \\bool\\<^sub>\\\<^sub>\ ### Ambiguous input (line 741 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclSize" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclSize" ("_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. ### Ambiguous input (line 775 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclIsEmpty" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclIsEmpty" ("_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. ### Ambiguous input (line 793 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclNotEmpty" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("_applC" ("_position" finite) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclNotEmpty" ("_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. ### Ambiguous input (line 798 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclNotEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" e) ### ("\<^const>Set.member" ("_position" e) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclNotEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" e) ### ("\<^const>Set.member" ("_position" e) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ### ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \)))))))))) ### 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 818 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 4 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIsEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclANY" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIsEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclANY" ("_position" X))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIsEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclANY" ("_position" X)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIsEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("\<^const>UML_Set.OclANY" ("_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. ### Ambiguous input (line 1003 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_lambda" ### ("_pttrns" ("_position" X) ### ("_pttrns" ("_position" St) ("_position" x))) ### ("_applC" ("_position" P) ### ("_cargs" ("_lambda" ("_position" \) ("_position" x)) ### ("_cargs" ("_position" X) ("_position" St))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" S))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_OclForallSet" ### ("_lambda" ("_position" X) ### ("_applC" ("_position" S) ("_position" X))) ### x ("_applC" ("_position" P) ### ("_cargs" ("_position" x) ("_position" X)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_lambda" ### ("_pttrns" ("_position" X) ### ("_pttrns" ("_position" St) ("_position" x))) ### ("_applC" ("_position" P) ### ("_cargs" ("_lambda" ("_position" \) ("_position" x)) ### ("_cargs" ("_position" X) ("_position" St))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" S))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" cp) ### ("_lambda" ("_position" X) ### ("_OclForallSet" ("_applC" ("_position" S) ("_position" X)) x ### ("_applC" ("_position" P) ### ("_cargs" ("_position" x) ("_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. ### Ambiguous input (line 1107 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_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. ### Ambiguous input (line 1124 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_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. ### Ambiguous input (line 1125 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ("_position" X) ("_position" x))) ### ("_position" X))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Set.OclIncluding" ("_position" X) ("_position" x)) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x)) ### ("_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. ### Ambiguous input (line 1250 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclExcludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclExcludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_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. ### Ambiguous input (line 1266 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclExcludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclExcludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_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. ### Ambiguous input (line 1267 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclExcluding" ("_position" X) ("_position" x))) ### ("_position" X))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Set.OclExcluding" ("_position" X) ("_position" x)) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x)) ### ("_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. ### Ambiguous input (line 1406 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclIncluding" ("_position" X) ("_position" x)) ### ("_position" y))) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" X) ("_position" y)) ### ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclIncluding" ("_position" X) ("_position" x)) ### ("_position" y)) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" X) ("_position" y)) ### ("_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. ### Ambiguous input (line 1686 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Set.OclIncluding" ("_position" X) ("_position" x)) ### ("_position" y))) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Set.OclIncluding" ("_position" X) ("_position" x)) ### ("_position" y)) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_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. ### Ambiguous input (line 1791 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" S) ### ("_constrain" ("_position" x) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" val)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" S)) ### ("_constrain" ("_position" x) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" val))))) ### 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 1792 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" S)) ### ("_constrain" ("_position" a) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" val)))) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Set.OclIncluding" ("_position" S) ### ("_constrain" ("_position" a) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" val)))) ### ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ("_position" S) ### ("_constrain" ("_position" a) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" val))))) ### ("_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. ### Ambiguous input (line 2882 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" OclForall) ### ("_cargs" ("_position" X) ("_position" P)))) ### ("\<^const>UML_Logic.OclValid" ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))) ### ("_position" \)) ### ("_applC" ("_position" P) ### ("_lambda" ("_position" \) ("_position" x)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" OclForall) ### ("_cargs" ("_position" X) ("_position" P)))) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" P) ### ("_lambda" ("_position" \) ("_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. ### Ambiguous input (line 3103 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 4 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" P))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_constrain" ("_position" x) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set)))) ### ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_constrain" ("_applC" ("_position" P) ("_position" x)) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set)))) ### ("_applC" ("_position" P) ("_position" y)))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" P))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ### ("_constrain" ("_position" x) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set))) ### ("_position" y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_constrain" ("_applC" ("_position" P) ("_position" x)) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set)))) ### ("_applC" ("_position" P) ("_position" y)))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" P))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_constrain" ("_position" x) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set)))) ### ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ### ("_constrain" ("_applC" ("_position" P) ("_position" x)) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set))) ### ("_applC" ("_position" P) ("_position" y))))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" cp) ("_position" P))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ### ("_applC" ("_position" P) ("_position" y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ### ("_constrain" ("_position" x) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set))) ### ("_position" y)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ### ("_constrain" ("_applC" ("_position" P) ("_position" x)) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" '\) ### ("_class_name" null)) ### ("_type_name" Set))) ### ("_applC" ("_position" P) ("_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. ### Ambiguous input (line 3126 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 6 parse trees: ### ("\<^const>Pure.all_binder" ### ("_idts" ### ("_idtyp" ("_position" s) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" Set))) ### ("_idts" ("_position" t) ### ("_idts" ("_position" x) ### ("_idts" ("_position" y) ("_position" \))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" s)) ### ("_position" t))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" x) ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ("_position" s) ### ("_position" x))) ### ("\<^const>UML_Set.OclIncluding" ("_position" t) ### ("_position" y))))))))) ### ("\<^const>Pure.all_binder" ### ("_idts" ### ("_idtyp" ("_position" s) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" Set))) ### ("_idts" ("_position" t) ### ("_idts" ("_position" x) ### ("_idts" ("_position" y) ("_position" \))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ("_position" s) ### ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" x) ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ("_position" s) ### ("_position" x))) ### ("\<^const>UML_Set.OclIncluding" ("_position" t) ### ("_position" y))))))))) ### ("\<^const>Pure.all_binder" ### ("_idts" ### ("_idtyp" ("_position" s) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" Set))) ### ("_idts" ("_position" t) ### ("_idts" ("_position" x) ### ("_idts" ("_position" y) ("_position" \))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" s)) ### ("_position" t))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" x) ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Set.OclIncluding" ("_position" s) ### ("_position" x)) ### ("\<^const>UML_Set.OclIncluding" ("_position" t) ### ("_position" y)))))))))) ### ("\<^const>Pure.all_binder" ### ("_idts" ### ("_idtyp" ("_position" s) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" Set))) ### ("_idts" ("_position" t) ### ("_idts" ("_position" x) ### ("_idts" ("_position" y) ("_position" \))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ("_position" s) ### ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" x) ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Set.OclIncluding" ("_position" s) ### ("_position" x)) ### ("\<^const>UML_Set.OclIncluding" ("_position" t) ### ("_position" y)))))))))) ### ("\<^const>Pure.all_binder" ### ("_idts" ### ("_idtyp" ("_position" s) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" Set))) ### ("_idts" ("_position" t) ### ("_idts" ("_position" x) ### ("_idts" ("_position" y) ("_position" \))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" s)) ### ("_position" t))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" x) ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" s)) ### ("_position" x)) ### ("\<^const>UML_Set.OclIncluding" ("_position" t) ### ("_position" y))))))))) ### ("\<^const>Pure.all_binder" ### ("_idts" ### ("_idtyp" ("_position" s) ### ("_tappl" ("_position_sort" '\) ### ("_ofsort" ("_position_sort" 'a) ("_class_name" null)) ### ("_type_name" Set))) ### ("_idts" ("_position" t) ### ("_idts" ("_position" x) ### ("_idts" ("_position" y) ("_position" \))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrictRefEq" ("_position" s) ### ("_position" t)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" x) ("_position" y))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrictRefEq" ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" s)) ### ("_position" x)) ### ("\<^const>UML_Set.OclIncluding" ("_position" t) ### ("_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. ### Ambiguous input (line 3138 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" const) ("_position" a))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" const) ("_position" S))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" const) ("_position" X))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" const) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.StrictRefEq" ("_position" X) ### ("_position" S)) ### ("_position" a))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" const) ("_position" a))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ("_applC" ("_position" const) ("_position" S))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" const) ("_position" X))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" const) ### ("\<^const>UML_Logic.StrictRefEq" ("_position" X) ### ("\<^const>UML_Set.OclIncluding" ("_position" S) ### ("_position" 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\<^sub>b\<^sub>a\<^sub>s\<^sub>e :: (equal) equal equal_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e == equal_class.equal :: Set('a) \ Set('a) \ bool ### Ambiguous input (line 3158 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 3 parse trees: ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Set.OclIncluding" ("\<^const>UML_Set.mtSet") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Integer.OclInt1"))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Set.OclIncluding" ("\<^const>UML_Set.mtSet") ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1")))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Set.mtSet")) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1"))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'm::{} not of sort type ### KO: 'nbe' failed to normalize ### Ambiguous input (line 3158 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Set.OclIncluding" ("\<^const>UML_Set.mtSet") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Integer.OclInt1")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Set.OclIncluding" ("\<^const>UML_Set.mtSet") ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Set.OclIncluding" ### ("\<^const>UML_Logic.StrongEq" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt1") ### ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Set.mtSet")) ### ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclInt1")))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ak::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ak::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### theory "Featherweight_OCL.UML_Set" ### 5.347s elapsed time, 10.640s cpu time, 0.632s GC time Loading theory "Featherweight_OCL.UML_Library" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts" via "Featherweight_OCL.UML_State") ### Ambiguous input (line 101 of "~~/afp/thys/Featherweight_OCL/UML_Library.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Library.OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l" ### ("\<^const>UML_Library.OclAsReal\<^sub>I\<^sub>n\<^sub>t" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("_position" X))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Library.OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l" ### ("\<^const>UML_Library.OclAsReal\<^sub>I\<^sub>n\<^sub>t" ### ("_position" X)))) ### ("_position" X))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Library.OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l" ### ("\<^const>UML_Library.OclAsReal\<^sub>I\<^sub>n\<^sub>t" ### ("_position" X))) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Library.OclAsInteger\<^sub>R\<^sub>e\<^sub>a\<^sub>l" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Library.OclAsReal\<^sub>I\<^sub>n\<^sub>t" ### ("_position" X)))) ### ("_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. ### Ignoring duplicate safe introduction (intro!) ### cp (\_. c) ### Ignoring duplicate rewrite rule: ### cp (\_. c1) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\X. X) ### Ignoring duplicate rewrite rule: ### cp (\X. X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. not (P X)) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. not (P1 X)) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X and Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X and Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X or Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X or Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X implies Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X implies Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X \ Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X \ Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q; cp R\ ### \ cp (\X. if P X then Q X else R X endif) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1; cp R1\ ### \ cp (\X. ### if P1 X then Q1 X else R1 X endif) \ ### True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->size\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->size\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->any\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->any\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. ### P X->including\<^sub>S\<^sub>e\<^sub>q(Q X)) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. ### P1 X->including\<^sub>S\<^sub>e\<^sub>q(Q1 ### X)) \ ### True ### Ignoring duplicate safe introduction (intro!) ### cp (\_. c) ### Ignoring duplicate rewrite rule: ### cp (\_. c1) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\X. X) ### Ignoring duplicate rewrite rule: ### cp (\X. X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. not (P X)) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. not (P1 X)) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X and Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X and Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X or Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X or Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X implies Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X implies Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X \ Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X \ Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q; cp R\ ### \ cp (\X. if P X then Q X else R X endif) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1; cp R1\ ### \ cp (\X. ### if P1 X then Q1 X else R1 X endif) \ ### True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->size\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->size\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->any\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->any\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. ### P X->including\<^sub>S\<^sub>e\<^sub>q(Q X)) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. ### P1 X->including\<^sub>S\<^sub>e\<^sub>q(Q1 ### X)) \ ### True ### Ambiguous input (line 207 of "~~/afp/thys/Featherweight_OCL/UML_Library.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Integer.OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" ### ("\<^const>UML_Integer.OclInt0") ("\<^const>UML_Integer.OclInt2"))) ### ("\<^const>UML_Integer.OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" ### ("\<^const>UML_Integer.OclInt0") ("\<^const>UML_Integer.OclInt1"))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Integer.OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" ### ("\<^const>UML_Integer.OclInt0") ("\<^const>UML_Integer.OclInt2")) ### ("\<^const>UML_Integer.OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" ### ("\<^const>UML_Integer.OclInt0") ("\<^const>UML_Integer.OclInt1")))) ### 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 230 of "~~/afp/thys/Featherweight_OCL/UML_Library.thy") produces 2 parse trees: ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_OclForallSet" ### ("\<^const>UML_Logic.defined" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt2") ("_position" null)))) ### z ("\<^const>UML_Integer.OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" ### ("\<^const>UML_Integer.OclInt0") ("_position" z))))) ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("_OclForallSet" ### ("_OclFinset" ### ("_args" ("\<^const>UML_Integer.OclInt2") ("_position" null))) ### z ("\<^const>UML_Integer.OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" ### ("\<^const>UML_Integer.OclInt0") ("_position" z)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ao::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ao::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ao::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'dq::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'fy::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ju::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\Set('b) set\\<^sub>\\\<^sub>\ ### \ \\Set('b) set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'oz::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ei::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable 'b::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'b set\\<^sub>\\\<^sub>\ ### \ \\'b set\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable 'b::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable 'ei::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### Type unification failed: Variable ?'a::{} not of sort type ### ### Failed to meet type constraint: ### ### Term: equal_class.equal :: ?'a \ ?'a \ bool ### Type: ### \\'a list\\<^sub>\\\<^sub>\ ### \ \\'a list\\<^sub>\\\<^sub>\ ### \ bool ### ### Coercion Inference: ### ### Local coercion insertion on the operand failed: ### Variable ?'a::{} not of sort type ### ### Now trying to infer coercions globally. ### ### Coercion inference failed: ### failed to unify invariant arguments ### Variable ?'a::{} not of sort type ### KO: 'nbe' failed to normalize OK: 'simp' finished the normalization ### theory "Featherweight_OCL.UML_Library" ### 46.033s elapsed time, 91.060s cpu time, 8.616s GC time Loading theory "Featherweight_OCL.UML_State" (required by "Featherweight_OCL.UML_Main" via "Featherweight_OCL.UML_Contracts") ### Ignoring duplicate safe introduction (intro!) ### cp (\_. c) ### Ignoring duplicate rewrite rule: ### cp (\_. c1) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\X. X) ### Ignoring duplicate rewrite rule: ### cp (\X. X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. not (P X)) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. not (P1 X)) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X and Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X and Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X or Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X or Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X implies Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X implies Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X \ Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X \ Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q; cp R\ ### \ cp (\X. if P X then Q X else R X endif) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1; cp R1\ ### \ cp (\X. ### if P1 X then Q1 X else R1 X endif) \ ### True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->size\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->size\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->any\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->any\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. ### P X->including\<^sub>S\<^sub>e\<^sub>q(Q X)) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. ### P1 X->including\<^sub>S\<^sub>e\<^sub>q(Q1 ### X)) \ ### True ### Ignoring duplicate safe introduction (intro!) ### cp (\_. c) ### Ignoring duplicate rewrite rule: ### cp (\_. c1) \ True ### Ignoring duplicate safe introduction (intro!) ### cp (\X. X) ### Ignoring duplicate rewrite rule: ### cp (\X. X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. \ P X) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. \ P1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. not (P X)) ### Ignoring duplicate rewrite rule: ### cp P1 \ cp (\X. not (P1 X)) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X and Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X and Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ \ cp (\X. P X or Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X or Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X implies Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X implies Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. P X \ Q X) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. P1 X \ Q1 X) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q; cp R\ ### \ cp (\X. if P X then Q X else R X endif) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1; cp R1\ ### \ cp (\X. ### if P1 X then Q1 X else R1 X endif) \ ### True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->size\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->size\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->isEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ ### cp (\X. P X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->notEmpty\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### cp P \ cp (\X. P X->any\<^sub>S\<^sub>e\<^sub>t()) ### Ignoring duplicate rewrite rule: ### cp P1 \ ### cp (\X. P1 X->any\<^sub>S\<^sub>e\<^sub>t()) \ True ### Ignoring duplicate safe introduction (intro!) ### \cp P; cp Q\ ### \ cp (\X. ### P X->including\<^sub>S\<^sub>e\<^sub>q(Q X)) ### Ignoring duplicate rewrite rule: ### \cp P1; cp Q1\ ### \ cp (\X. ### P1 X->including\<^sub>S\<^sub>e\<^sub>q(Q1 ### X)) \ ### True ### Ambiguous input (line 234 of "~~/afp/thys/Featherweight_OCL/UML_State.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \\<^sub>0) ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H)))) ### ("\<^const>UML_Set.mtSet"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \\<^sub>0) ### ("\<^const>UML_Logic.StrongEq" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H))) ### ("\<^const>UML_Set.mtSet")))) ### 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 261 of "~~/afp/thys/Featherweight_OCL/UML_State.thy") produces 5 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H))))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" x))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>HOL.conj" ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H)))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" x)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.conj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H))))) ### ("_position" \)) ### ("\<^const>UML_Logic.defined" ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>HOL.conj" ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H)))) ### ("_position" \))) ### ("\<^const>UML_Logic.defined" ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.conj" ### ("\<^const>UML_Logic.defined" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H)))) ### ("_position" \)) ### ("\<^const>UML_Logic.defined" ("_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. ### Ambiguous input (line 272 of "~~/afp/thys/Featherweight_OCL/UML_State.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H))) ### ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("_position" OclAllInstances_generic) ### ("_cargs" ("_position" pre_post) ("_position" H)))) ### ("_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. ### theory "Featherweight_OCL.UML_State" ### 0.644s elapsed time, 1.288s cpu time, 0.000s GC time Loading theory "Featherweight_OCL.UML_Tools" (required by "Featherweight_OCL.UML_Main") val ocl_subst_asm_tac = fn: Proof.context -> int -> tactic val ocl_subst_asm = fn: Proof.context -> Method.method ### theory "Featherweight_OCL.UML_Tools" ### 0.092s elapsed time, 0.184s cpu time, 0.000s GC time ### Ignoring duplicate rewrite rule: ### UML_Types.bot_class.bot \ \ ### Ignoring duplicate rewrite rule: ### const \ \ True ### Ignoring duplicate rewrite rule: ### const null \ True ### Ignoring duplicate rewrite rule: ### const invalid \ True ### Ignoring duplicate rewrite rule: ### const false \ True ### Ignoring duplicate rewrite rule: ### const true \ True ### Ignoring duplicate rewrite rule: ### const \ \ True ### Ignoring duplicate rewrite rule: ### const null \ True ### Ignoring duplicate rewrite rule: ### const invalid \ True ### Ignoring duplicate rewrite rule: ### const false \ True ### Ignoring duplicate rewrite rule: ### const true \ True ### Ambiguous input (line 193 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Integer.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.defined" ("_position" x)))))) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_applC" ("_position" x) ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" x))))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.defined" ("_position" x)))))) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_applC" ("_position" x) ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \))) ### ("_position" \)) ### ("\<^const>UML_Logic.defined" ("_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. ### Ignoring duplicate rewrite rule: ### bin f1 g1 \ bin' f1 (\X Y \. g1 (X \) (Y \)) ### Ignoring duplicate rewrite rule: ### bin' f1 g1 d\<^sub>x1 d\<^sub>y1 X1 Y1 \ ### f1 X1 Y1 = ### (\\. ### if d\<^sub>x1 X1 \ = true \ \ ### d\<^sub>y1 Y1 \ = true \ ### then g1 X1 Y1 \ else invalid \) ### Metis: Unused theorems: "UML_Logic.valid_def" ### Metis: Unused theorems: "UML_Logic.valid_def" ### Metis: Unused theorems: "UML_Logic.valid_def" ### Metis: Unused theorems: "UML_Logic.valid_def" ### Ambiguous input (line 194 of "~~/afp/thys/Featherweight_OCL/basic_types/UML_Real.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.defined" ("_position" x)))))) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_applC" ("_position" x) ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" x))))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_applC" ("\<^const>UML_Logic.OclNot") ### ("\<^const>UML_Logic.defined" ("_position" x)))))) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_applC" ("_position" x) ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \))) ### ("_position" \)) ### ("\<^const>UML_Logic.defined" ("_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. ### Ambiguous input (line 140 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 10 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" ### Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### 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 146 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 10 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" ### Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Metis: Unused theorems: "UML_Logic.OclValid_def", "UML_Logic.true_def" ### Ambiguous input (line 149 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 10 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" ### Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### 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 161 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less" ### ("\<^const>Groups.zero_class.zero") ### ("_applC" ("_position" aa) ### ("_applC" ("_position" Abs_Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" None)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" V)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.ApproxEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" aa) ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>Groups.zero_class.zero"))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less" ### ("\<^const>Groups.zero_class.zero") ### ("_applC" ("_position" aa) ### ("_applC" ("_position" Abs_Void\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" None)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" V)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.ApproxEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l)))))))) ### 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 761 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Bag.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Bag.OclNotEmpty" ("_position" X)))) ### ("\<^const>HOL.Trueprop" ("_position" ?thesis)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Bag.OclNotEmpty" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X)))) ### ("\<^const>HOL.Trueprop" ("_position" ?thesis)))) ### 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 132 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 10 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" ### Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_position" y)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ("_position" y) ### ("_Coll" ("_position" X) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ### ("\<^const>UML_Types.bot_class.bot")) ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" X) ("_position" null)) ### ("_Ball" ("_position" x) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ("_position" X))) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### 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 138 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 10 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" ### Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ("_position" a))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("\<^const>UML_Types.drop" ("_position" a)) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Metis: Unused theorems: "UML_Logic.OclValid_def", "UML_Logic.true_def" ### Ambiguous input (line 141 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 10 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" ### Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V)))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l) ### ("_position" \)) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" V))) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" V) ("_position" \)) ### ("_applC" ("_position" Abs_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("\<^const>Option.option.Some" ### ("\<^const>Option.option.Some" ("_position" aa)))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("_Ball" ("_position" x) ("_position" aa) ### ("\<^const>HOL.not_equal" ("_position" x) ### ("\<^const>UML_Types.bot_class.bot")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.disj" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" V) ### ("_position" Void\<^sub>n\<^sub>u\<^sub>l\<^sub>l))) ### ("_position" \)) ### ("_position" V)) ### ("_position" Void\<^sub>e\<^sub>m\<^sub>p\<^sub>t\<^sub>y))))) ### 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 1110 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_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. ### Metis: Unused theorems: "UML_Types.bot_fun_def" ### Ambiguous input (line 1113 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_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. ### Ambiguous input (line 1253 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclExcludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclExcludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_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. ### Ambiguous input (line 1256 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclExcludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclExcludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_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. ### Ambiguous input (line 1344 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" i)) ### ("_position" invalid))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" i) ### ("_position" invalid)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1347 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" i)) ### ("_position" invalid))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" i) ### ("_position" invalid)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1350 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" j)) ### ("_position" invalid))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" j) ### ("_position" invalid)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1353 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" j)) ### ("_position" invalid))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" j) ### ("_position" invalid)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" S)) ### ("_position" invalid))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" S) ### ("_position" invalid)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1359 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" S)) ### ("_position" invalid))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" S) ### ("_position" invalid)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1362 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" S)) ### ("_position" null))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" S) ("_position" null)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" i)) ### ("_position" j)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1365 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.StrongEq" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" S)) ### ("_position" null))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### ("\<^const>Pure.all_binder" ("_position" \) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.StrongEq" ("_position" S) ("_position" null)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ### ("\<^const>UML_Set.OclExcluding" ### ("\<^const>UML_Set.OclExcluding" ("_position" S) ### ("_position" j)) ### ("_position" i)) ### ("_position" \)) ### ("_applC" ("_position" invalid) ("_position" \)))))) ### 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 1868 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 5 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))) ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.not_member" ### ("_applC" ("_position" x) ("_position" \)) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("_position" X))) ### ("_position" x))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))) ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.not_member" ### ("_applC" ("_position" x) ("_position" \)) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("\<^const>HOL.Not" ("_position" \)) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))) ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.not_member" ### ("_applC" ("_position" x) ("_position" \)) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Not" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))) ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.not_member" ### ("_applC" ("_position" x) ("_position" \)) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ### ("\<^const>HOL.Not" ("_position" \)) ("_position" X)) ### ("_position" x))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.defined" ("_position" X)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))) ### ("\<^const>HOL.eq" ### ("_applC" ("\<^const>UML_Logic.valid" ("_position" x)) ### ("_position" \)) ### ("_applC" ("_position" true) ("_position" \))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.not_member" ### ("_applC" ("_position" x) ("_position" \)) ### ("\<^const>UML_Types.drop" ### ("\<^const>UML_Types.drop" ### ("_applC" ("_position" Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e) ### ("_applC" ("_position" X) ("_position" \))))))))) ### 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 1872 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_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. ### Metis: Unused theorems: "UML_Types.bot_fun_def" ### Ambiguous input (line 1875 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_position" x))))) ### ("\<^const>Pure.imp" ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_position" x))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.valid" ("_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. ### Metis: Unused theorems: "UML_Logic.foundation5" ### Ambiguous input (line 1888 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.defined" ("_position" X))) ### ("\<^const>UML_Logic.valid" ("_position" x))) ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Logic.OclAnd" ### ("\<^const>UML_Logic.defined" ("_position" X)) ### ("\<^const>UML_Logic.valid" ("_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. ### Ambiguous input (line 1890 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>UML_Logic.OclValid" ("_position" \) ### ("\<^const>UML_Set.OclIncludes" ("_position" X) ("_position" x))) ### ("\<^const>UML_Set.OclIncludes" ### ("\<^const>UML_Logic.OclValid" ("_position" \) ("_position" X)) ### ("_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. ### Ambiguous input (line 1892 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>UML_Set.OclSize" ("\<^const>UML_Logic.valid" ("_position" X))) ### ("\<^const>UML_Logic.valid" ("\<^const>UML_Set.OclSize" ("_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. ### Ambiguous input (line 1892 of "~~/afp/thys/Featherweight_OCL/collection_types/UML_Set.thy") produces 2 parse trees: ### ("\<^const>UML_Set.OclSize" ("\<^const>UML_Logic.valid" ("_position" X))) ### ("\<^const>UML_Logic.valid" ("\<^const>UML_Set.OclSize" ("_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. ### Metis: Unused theorems: "UML_Logic.OclAnd_idem", "UML_Logic.OclImplies_def", "UML_Logic.deMorgan2" ### Metis: Unused theorems: "UML_Types.null_option_def" ### Metis: Unused theorems: "UML_Types.invalid_def" ### Metis: Unused theorems: "UML_Types.null_fun_def" ### Metis: Unused theorems: "Set.subset_antisym" ### Ignoring duplicate rewrite rule: ### X1->including\<^sub>S\<^sub>e\<^sub>t(x1)->includes\<^sub>S\<^sub>e\<^sub>t(y1) \ ### if \ X1 then if x1 \ ### y1 then true else X1->includes\<^sub>S\<^sub>e\<^sub>t(y1) endif else invalid endif ### Ignoring duplicate rewrite rule: ### const \ \ True ### Ignoring duplicate rewrite rule: ### const null \ True ### Ignoring duplicate rewrite rule: ### const invalid \ True ### Ignoring duplicate rewrite rule: ### const false \ True ### Ignoring duplicate rewrite rule: ### const true \ True ### Ignoring duplicate rewrite rule: ### const \ \ True ### Ignoring duplicate rewrite rule: ### const null \ True ### Ignoring duplicate rewrite rule: ### const invalid \ True ### Ignoring duplicate rewrite rule: ### const false \ True ### Ignoring duplicate rewrite rule: ### const true \ True \\ \ y \ x; cp P; \ \ P x\ \ \ \ P y \\ \ not (\ y); cp P; \ \ P invalid\ \ \ \ P y \\ |\ \ y; cp P; \ \ P invalid\ \ \ \ P y \\ \ not y; cp P; \ \ P false\ \ \ \ P y \\ \ y; cp P; \ \ P true\ \ \ \ P y \\ \ x \ y; cp P\ \ (\ \ P x) = (\ \ P y) \\ \ not (\ x); cp P\ \ (\ \ P x) = (\ \ P invalid) \\ |\ \ x; cp P\ \ (\ \ P x) = (\ \ P invalid) \\ \ not x; cp P\ \ (\ \ P x) = (\ \ P false) \\ \ x; cp P\ \ (\ \ P x) = (\ \ P true) \\ \ x \ y; cp P; \ |\ P y\ \ \ |\ P x \\ \ not (\ x); cp P; \ |\ P invalid\ \ \ |\ P x \\ |\ \ x; cp P; \ |\ P invalid\ \ \ |\ P x \\ \ not x; cp P; \ |\ P false\ \ \ |\ P x \\ \ x; cp P; \ |\ P true\ \ \ |\ P x \\ \ x \ y; cp P\ \ (\ |\ P x) = (\ |\ P y) \\ \ not (\ x); cp P\ \ (\ |\ P x) = (\ |\ P invalid) \\ |\ \ x; cp P\ \ (\ |\ P x) = (\ |\ P invalid) \\ \ not x; cp P\ \ (\ |\ P x) = (\ |\ P false) \\ \ x; cp P\ \ (\ |\ P x) = (\ |\ P true) x = y \ (\ x) = (\ y) isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/annex-a -o pdf -n annex-a -t annexa,-theory,-afp,-proof,-ML isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/document -o pdf -n document -t afp,-annexa *** Failed to load theory "Featherweight_OCL.UML_Contracts" (unresolved "Featherweight_OCL.UML_State") *** Failed to load theory "Featherweight_OCL.UML_Main" (unresolved "Featherweight_OCL.UML_Contracts") *** Failed to load theory "Featherweight_OCL.Analysis_UML" (unresolved "Featherweight_OCL.UML_Main") *** Failed to load theory "Featherweight_OCL.Analysis_OCL" (unresolved "Featherweight_OCL.Analysis_UML") *** Failed to load theory "Featherweight_OCL.Design_UML" (unresolved "Featherweight_OCL.UML_Main") *** Failed to load theory "Featherweight_OCL.Design_OCL" (unresolved "Featherweight_OCL.Design_UML") *** Latex error: *** File `UML_Contracts.tex' not found. *** Latex error (line 251 of "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/annex-a/root.tex"): *** Emergency stop. *** *** *** \input{UML_Contracts.tex} *** Latex error (line 251 of "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/annex-a/root.tex"): *** ==> Fatal error occurred, no output PDF file produced! *** Failed to build document in "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Featherweight_OCL/annex-a" *** Ambiguous input (line 294 of "~~/afp/thys/Featherweight_OCL/UML_State.thy") produces 2 parse trees: *** ("\<^const>HOL.Trueprop" *** ("\<^const>UML_Logic.StrictRefEq" *** ("\<^const>UML_Logic.OclValid" *** ("_applC" ("_position" mk) *** ("_record" *** ("_fields" ("_field" ("_constify" heap) ("_position" empty)) *** ("_field" ("_constify" assocs) ("_position" A))))) *** ("_applC" ("_position" OclAllInstances_generic) *** ("_cargs" ("_position" pre_post) ("_position" Type)))) *** ("\<^const>UML_Set.mtSet"))) *** ("\<^const>HOL.Trueprop" *** ("\<^const>UML_Logic.OclValid" *** ("_applC" ("_position" mk) *** ("_record" *** ("_fields" ("_field" ("_constify" heap) ("_position" empty)) *** ("_field" ("_constify" assocs) ("_position" A))))) *** ("\<^const>UML_Logic.StrictRefEq" *** ("_applC" ("_position" OclAllInstances_generic) *** ("_cargs" ("_position" pre_post) ("_position" Type))) *** ("\<^const>UML_Set.mtSet")))) *** At command "lemma" (line 292 of "~~/afp/thys/Featherweight_OCL/UML_State.thy") *** Type unification failed: Clash of types "_ set" and "_ \ _" *** *** Type error in application: incompatible operand type *** *** Operator: state_ext :: *** (nat \ \?'a\\<^sub>\) *** \ (nat *** \ \nat list list list\\<^sub>\) *** \ ?'b \ (?'a, ?'b) state_scheme *** Operand: {} :: ?'c set *** *** Coercion Inference: *** *** Local coercion insertion on the operand failed: *** No coercion known for type constructors: "set" and "fun" *** At command "lemma" (line 292 of "~~/afp/thys/Featherweight_OCL/UML_State.thy") *** Type unification failed: Clash of types "_ set" and "_ \ _" *** *** Type error in application: incompatible operand type *** *** Operator: state_ext :: *** (nat \ \?'a\\<^sub>\) *** \ (nat *** \ \nat list list list\\<^sub>\) *** \ ?'b \ (?'a, ?'b) state_scheme *** Operand: {} :: ?'c set *** *** Coercion Inference: *** *** Local coercion insertion on the operand failed: *** No coercion known for type constructors: "set" and "fun" *** At command "lemma" (line 292 of "~~/afp/thys/Featherweight_OCL/UML_State.thy")