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.164s elapsed time, 0.700s cpu time, 0.000s GC time ### theory "Safe_OCL.Errorable" ### 0.273s elapsed time, 1.144s cpu time, 0.000s GC time ### theory "Safe_OCL.Finite_Map_Ext" ### 0.335s elapsed time, 1.372s cpu time, 0.000s GC time Loading theory "Safe_OCL.Tuple" Loading theory "Safe_OCL.Object_Model" ### theory "Safe_OCL.Tuple" ### 0.530s elapsed time, 2.112s 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'" Proofs for inductive predicate(s) "basic_subtype" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... 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" 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 ... 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 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" 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'" 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) "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" 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 ... Found termination order: "{}" 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 ... 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 ... Found termination order: "{}" ### theory "Safe_OCL.OCL_Basic_Types" ### 3.321s elapsed time, 13.008s cpu time, 0.992s 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") 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.431s elapsed time, 21.120s cpu time, 1.072s GC time ### theory "Safe_OCL.Object_Model" ### 15.933s elapsed time, 45.684s cpu time, 2.368s 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" ### 28.160s elapsed time, 54.116s cpu time, 2.640s 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.197s elapsed time, 0.364s 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" ### 31.158s elapsed time, 42.760s cpu time, 1.840s 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" ### 5.922s elapsed time, 9.824s cpu time, 0.316s 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" ### 1.972s elapsed time, 3.696s 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/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Safe_OCL/document -o pdf -n document *** 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")