Loading theory "Safe_OCL.Transitive_Closure_Ext" Loading theory "Safe_OCL.Finite_Map_Ext" Loading theory "Safe_OCL.Errorable" Loading theory "Safe_OCL.OCL_Basic_Types" (required by "Safe_OCL.OCL_Examples" via "Safe_OCL.OCL_Normalization" via "Safe_OCL.OCL_Typing" via "Safe_OCL.OCL_Object_Model" via "Safe_OCL.OCL_Syntax" via "Safe_OCL.OCL_Types") instantiation errorable :: (type) bot bot_errorable == bot :: 'a\<^sub>\ ### theory "Safe_OCL.Transitive_Closure_Ext" ### 0.142s elapsed time, 0.620s cpu time, 0.000s GC time ### theory "Safe_OCL.Errorable" ### 0.263s elapsed time, 1.112s cpu time, 0.000s GC time ### theory "Safe_OCL.Finite_Map_Ext" ### 0.298s elapsed time, 1.240s cpu time, 0.000s GC time Loading theory "Safe_OCL.Tuple" Loading theory "Safe_OCL.Object_Model" ### theory "Safe_OCL.Tuple" ### 0.523s elapsed time, 2.088s cpu time, 0.000s GC time Proofs for inductive predicate(s) "owned_attribute'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "attribute_not_closest" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "closest_attribute" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "closest_attribute_not_unique" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unique_closest_attribute" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "role_refer_class" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "association_ends'" Proofs for inductive predicate(s) "basic_subtype" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving monotonicity ... Proving the simplification rules ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "association_ends_not_unique'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "owned_association_end'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation basic_type :: (order) order less_eq_basic_type == less_eq :: 'a basic_type \ 'a basic_type \ bool less_basic_type == less :: 'a basic_type \ 'a basic_type \ bool Proofs for inductive predicate(s) "association_end_not_closest" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "closest_association_end" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "closest_association_end_not_unique" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unique_closest_association_end" instantiation basic_type :: (semilattice_sup) semilattice_sup sup_basic_type == sup :: 'a basic_type \ 'a basic_type \ 'a basic_type Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "referred_by_association_class''" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "referred_by_association_class'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "association_class_not_closest" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "closest_association_class" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "closest_association_class_not_unique" Found termination order: "{}" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unique_closest_association_class" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "association_class_end'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "association_class_end_not_unique" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unique_association_class_end" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "any_operation'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "operation'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "operation_not_unique" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unique_operation" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "operation_defined'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "{}" Proofs for inductive predicate(s) "static_operation'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Safe_OCL.OCL_Basic_Types" ### 3.258s elapsed time, 12.748s cpu time, 1.092s GC time Loading theory "Safe_OCL.OCL_Types" (required by "Safe_OCL.OCL_Examples" via "Safe_OCL.OCL_Normalization" via "Safe_OCL.OCL_Typing" via "Safe_OCL.OCL_Object_Model" via "Safe_OCL.OCL_Syntax") Proofs for inductive predicate(s) "static_operation_not_unique" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unique_static_operation" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "static_operation_defined'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "has_literal'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale object_model fixes classes :: "'a fset" and attributes :: "'a \\<^sub>f String.literal \\<^sub>f 't" and associations :: "String.literal \\<^sub>f String.literal \\<^sub>f ('a \ nat \ enat \ bool \ bool)" and association_classes :: "'a \\<^sub>f String.literal" and operations :: "(String.literal \ 't \ (String.literal \ 't \ param_dir) list \ 't \ bool \ 'e option) list" and literals :: "'n \\<^sub>f String.literal fset" assumes "object_model classes associations" instantiation OCL_Types.type :: (type) size size_type == size :: 'a OCL_Types.type \ nat consts size_type :: "'a OCL_Types.type \ nat" Proofs for inductive predicate(s) "subtype" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation OCL_Types.type :: (order) order less_eq_type == less_eq :: 'a OCL_Types.type \ 'a OCL_Types.type \ bool less_type == less :: 'a OCL_Types.type \ 'a OCL_Types.type \ bool instantiation OCL_Types.type :: (semilattice_sup) semilattice_sup sup_type == sup :: 'a OCL_Types.type \ 'a OCL_Types.type \ 'a OCL_Types.type Found termination order: "(\p. size (snd p)) <*mlex*> {}" Proofs for inductive predicate(s) "element_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "update_element_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "to_unique_collection" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "to_nonunique_collection" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "to_ordered_collection" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "size <*mlex*> {}" Found termination order: "{}" Found termination order: "size <*mlex*> {}" ### theory "Safe_OCL.OCL_Types" ### 5.405s elapsed time, 20.984s cpu time, 0.940s GC time ### theory "Safe_OCL.Object_Model" ### 16.422s elapsed time, 45.896s cpu time, 2.324s GC time Loading theory "Safe_OCL.OCL_Syntax" (required by "Safe_OCL.OCL_Examples" via "Safe_OCL.OCL_Normalization" via "Safe_OCL.OCL_Typing" via "Safe_OCL.OCL_Object_Model") instantiation unat :: infinity infinity_unat == infinity :: unat ### theory "Safe_OCL.OCL_Syntax" ### 29.778s elapsed time, 56.116s cpu time, 2.740s GC time Loading theory "Safe_OCL.OCL_Object_Model" (required by "Safe_OCL.OCL_Examples" via "Safe_OCL.OCL_Normalization" via "Safe_OCL.OCL_Typing") class ocl_object_model = semilattice_sup + fixes classes :: "'a fset" and attributes :: "'a \\<^sub>f String.literal \\<^sub>f 'a OCL_Types.type" and associations :: "String.literal \\<^sub>f String.literal \\<^sub>f ('a \ nat \ enat \ bool \ bool)" and association_classes :: "'a \\<^sub>f String.literal" and operations :: "(String.literal \ 'a OCL_Types.type \ (String.literal \ 'a OCL_Types.type \ param_dir) list \ 'a OCL_Types.type \ bool \ 'a expr option) list" and literals :: "('a, String.literal) phantom \\<^sub>f String.literal fset" assumes "assoc_end_min_less_eq_max": "\assoc ends role end. \assoc |\| fmdom associations; fmlookup associations assoc = Some ends; role |\| fmdom ends; fmlookup ends role = Some end\ \ enat (assoc_end_min end) \ assoc_end_max end" assumes "association_ends_unique": "\\ from role end\<^sub>1 end\<^sub>2. \association_ends' classes associations \ from role end\<^sub>1; association_ends' classes associations \ from role end\<^sub>2\ \ end\<^sub>1 = end\<^sub>2" ### theory "Safe_OCL.OCL_Object_Model" ### 0.334s elapsed time, 0.760s cpu time, 0.364s GC time Loading theory "Safe_OCL.OCL_Typing" (required by "Safe_OCL.OCL_Examples" via "Safe_OCL.OCL_Normalization") Proofs for inductive predicate(s) "mataop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "typeop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "super_binop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "any_unop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "boolean_unop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "boolean_binop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "numeric_unop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "numeric_binop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "string_unop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "string_binop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "string_ternop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "collection_unop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "collection_binop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "collection_ternop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "unop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "binop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "ternop_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "op_type" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "typing", "collection_parts_typing", "collection_part_typing", "iterator_typing", "expr_list_typing" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Safe_OCL.OCL_Typing" ### 34.102s elapsed time, 46.124s cpu time, 1.396s GC time Loading theory "Safe_OCL.OCL_Normalization" (required by "Safe_OCL.OCL_Examples") Found termination order: "size <*mlex*> {}" Proofs for inductive predicate(s) "normalize", "normalize_call", "normalize_expr_list" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "nf_typing" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Safe_OCL.OCL_Normalization" ### 6.690s elapsed time, 10.732s cpu time, 0.244s GC time Loading theory "Safe_OCL.OCL_Examples" Proofs for inductive predicate(s) "subclass1" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... instantiation classes1 :: semilattice_sup sup_classes1 == sup :: classes1 \ classes1 \ classes1 less_eq_classes1 == less_eq :: classes1 \ classes1 \ bool less_classes1 == less :: classes1 \ classes1 \ bool Found termination order: "{}" Found termination order: "{}" instantiation classes1 :: ocl_object_model classes_classes1 == classes :: classes1 fset attributes_classes1 == attributes :: classes1 \\<^sub>f String.literal \\<^sub>f classes1 OCL_Types.type associations_classes1 == associations :: String.literal \\<^sub>f String.literal \\<^sub>f (classes1 \ nat \ enat \ bool \ bool) association_classes_classes1 == association_classes :: classes1 \\<^sub>f String.literal operations_classes1 == operations :: (String.literal \ classes1 OCL_Types.type \ (String.literal \ classes1 OCL_Types.type \ param_dir) list \ classes1 OCL_Types.type \ bool \ classes1 expr option) list literals_classes1 == literals :: (classes1, String.literal) phantom \\<^sub>f String.literal fset ### theory "Safe_OCL.OCL_Examples" ### 2.119s elapsed time, 3.936s cpu time, 0.000s GC time *** Failed to apply initial proof method (line 215 of "$AFP/Safe_OCL/OCL_Examples.thy"): *** goal: *** No subgoals! *** At command "by" (line 215 of "$AFP/Safe_OCL/OCL_Examples.thy") "{(Employee, String[1])}" :: "(classes1 \ classes1 OCL_Types.type) set" "{(Employee, Employee, 3, 7, False, False)}" :: "(classes1 \ classes1 \ nat \ enat \ bool \ bool) set" "{(Employee, Employee, 3, 7, False, False), (Employee, Employee, 3, 7, False, False)}" :: "(classes1 \ classes1 \ nat \ enat \ bool \ bool) set" "True" :: "bool" "{}" :: "(classes1 \ classes1 OCL_Types.type) set" "False" :: "bool" "{(STR ''membersCount'', \Project\\<^sub>\[1], [], Integer[1], False, Some (OperationCall (AssociationEndCall (Var STR ''self'') DotCall None STR ''members'') ArrowCall (Inl (Inr (Inr (Inr (Inr CollectionSizeOp))))) []))}" :: "(String.literal \ classes1 OCL_Types.type \ (String.literal \ classes1 OCL_Types.type \ param_dir) list \ classes1 OCL_Types.type \ bool \ classes1 expr option) set" "{(STR ''membersByName'', \Project\\<^sub>\[1], [(STR ''mn'', String[1], In)], Set \Employee\\<^sub>\[1], False, Some (SelectIteratorCall (AssociationEndCall (Var STR ''self'') DotCall None STR ''members'') ArrowCall [STR ''member''] None (OperationCall (AttributeCall (Var STR ''member'') DotCall STR ''name'') DotCall (Inr (Inl (Inl EqualOp))) [Var STR ''mn''])))}" :: "(String.literal \ classes1 OCL_Types.type \ (String.literal \ classes1 OCL_Types.type \ param_dir) list \ classes1 OCL_Types.type \ bool \ classes1 expr option) set" "{Bag \Employee\\<^sub>\[1]}" :: "classes1 OCL_Types.type set" "{}" :: "classes1 OCL_Types.type set" isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Safe_OCL/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Safe_OCL/outline -o pdf -n outline -t /proof,/ML *** Failed to apply initial proof method (line 215 of "$AFP/Safe_OCL/OCL_Examples.thy"): *** goal: *** No subgoals! *** At command "by" (line 215 of "$AFP/Safe_OCL/OCL_Examples.thy")