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") Loading theory "Safe_OCL.Transitive_Closure_Ext" instantiation errorable :: (type) bot bot_errorable == bot :: 'a\<^sub>\ ### theory "Safe_OCL.Transitive_Closure_Ext" ### 0.100s elapsed time, 0.444s cpu time, 0.000s GC time ### theory "Safe_OCL.Errorable" ### 0.241s elapsed time, 1.012s cpu time, 0.000s GC time ### theory "Safe_OCL.Finite_Map_Ext" ### 0.398s elapsed time, 1.620s cpu time, 0.000s GC time Loading theory "Safe_OCL.Tuple" Loading theory "Safe_OCL.Object_Model" ### theory "Safe_OCL.Tuple" ### 0.759s elapsed time, 3.004s 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'" 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_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 ... Proofs for inductive predicate(s) "association_end_not_closest" Proofs for inductive predicate(s) "basic_subtype" Proving monotonicity ... Proving monotonicity ... Proving the introduction rules ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the elimination rules ... Proving the simplification 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 ... 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) "unique_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) "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" 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) "closest_association_class_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_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 ... Found termination order: "{}" 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 ... 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 ... 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" Found termination order: "{}" ### theory "Safe_OCL.OCL_Basic_Types" ### 3.929s elapsed time, 15.504s cpu time, 1.236s 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") 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" ### 6.637s elapsed time, 25.604s cpu time, 0.928s GC time ### theory "Safe_OCL.Object_Model" ### 18.801s elapsed time, 53.184s cpu time, 2.420s 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" ### 37.897s elapsed time, 63.052s cpu time, 3.432s 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.229s elapsed time, 0.340s cpu time, 0.000s 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" ### 39.553s elapsed time, 51.216s cpu time, 1.280s 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" ### 7.689s elapsed time, 12.008s cpu time, 0.192s 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.877s elapsed time, 4.688s 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")