Loading theory "CoreC++.Auxiliary" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects" via "CoreC++.SubObj" via "CoreC++.ClassRel" via "CoreC++.Decl" via "CoreC++.Expr" via "CoreC++.Value" via "CoreC++.Type") ### Ignoring duplicate safe elimination (elim!) ### \?x # ?xs = map ?f ?ys; ### \z zs. ### ?ys = z # zs \ ?x = ?f z \ ?xs = map ?f zs \ ### PROP ?W\ ### \ PROP ?W ### Ignoring duplicate safe elimination (elim!) ### \?x # ?xs = map ?f ?ys; ### \z zs. ### ?ys = z # zs \ ?x = ?f z \ ?xs = map ?f zs \ ### PROP ?W\ ### \ PROP ?W ### theory "CoreC++.Auxiliary" ### 0.501s elapsed time, 0.808s cpu time, 0.000s GC time Loading theory "CoreC++.Type" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects" via "CoreC++.SubObj" via "CoreC++.ClassRel" via "CoreC++.Decl" via "CoreC++.Expr" via "CoreC++.Value") ### Ignoring duplicate rewrite rule: ### (?f1(?x1 := ?y1)) ?z1 \ if ?z1 = ?x1 then ?y1 else ?f1 ?z1 consts getbase :: "base \ char list" consts isRepBase :: "base \ bool" consts isShBase :: "base \ bool" ### theory "CoreC++.Type" ### 1.477s elapsed time, 2.668s cpu time, 0.000s GC time Loading theory "CoreC++.Value" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects" via "CoreC++.SubObj" via "CoreC++.ClassRel" via "CoreC++.Decl" via "CoreC++.Expr") ### No equation for constructor "Unit" ### No equation for constructor "Null" ### No equation for constructor "Bool" ### No equation for constructor "Ref" consts the_Intg :: "val \ int" ### No equation for constructor "Unit" ### No equation for constructor "Null" ### No equation for constructor "Bool" ### No equation for constructor "Intg" consts the_addr :: "val \ nat" ### No equation for constructor "Unit" ### No equation for constructor "Null" ### No equation for constructor "Bool" ### No equation for constructor "Intg" consts the_path :: "val \ char list list" consts default_val :: "ty \ val" consts typeof :: "val \ ty option" ### theory "CoreC++.Value" ### 0.921s elapsed time, 1.284s cpu time, 0.248s GC time Loading theory "CoreC++.Expr" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects" via "CoreC++.SubObj" via "CoreC++.ClassRel" via "CoreC++.Decl") Found termination order: "{}" ### Ambiguous input (line 80 of "~~/afp/thys/CoreC++/Expr.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_Update" ("_position" fv) ### ("_updbind" ("_position" V) ("_position" e))) ### ("\<^const>Set.union" ("_Finset" ("_position" V)) ### ("_applC" ("_position" fv) ("_position" e))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" fv) ### ("\<^const>Expr.expr.LAss" ("_position" V) ("_position" e))) ### ("\<^const>Set.union" ("_Finset" ("_position" V)) ### ("_applC" ("_position" fv) ("_position" e))))) ### 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 82 of "~~/afp/thys/CoreC++/Expr.thy") produces 3 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_Update" ("_position" fv) ### ("_updbind" ### ("\<^const>Expr.expr.FAcc" ("_position" e\<^sub>1) ("_position" F) ### ("_position" Cs)) ### ("_position" e\<^sub>2))) ### ("\<^const>Set.union" ### ("_applC" ("_position" fv) ("_position" e\<^sub>1)) ### ("_applC" ("_position" fv) ("_position" e\<^sub>2))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" fv) ### ("\<^const>Expr.expr.LAss" ### ("\<^const>Expr.expr.FAcc" ("_position" e\<^sub>1) ("_position" F) ### ("_position" Cs)) ### ("_position" e\<^sub>2))) ### ("\<^const>Set.union" ### ("_applC" ("_position" fv) ("_position" e\<^sub>1)) ### ("_applC" ("_position" fv) ("_position" e\<^sub>2))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" fv) ### ("\<^const>Expr.expr.FAss" ("_position" e\<^sub>1) ("_position" F) ### ("_position" Cs) ("_position" e\<^sub>2))) ### ("\<^const>Set.union" ### ("_applC" ("_position" fv) ("_position" e\<^sub>1)) ### ("_applC" ("_position" fv) ("_position" e\<^sub>2))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. consts fv :: "expr \ char list set" fvs :: "expr list \ char list set" ### theory "CoreC++.Expr" ### 5.366s elapsed time, 9.904s cpu time, 0.492s GC time Loading theory "CoreC++.Decl" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects" via "CoreC++.SubObj" via "CoreC++.ClassRel") ### theory "CoreC++.Decl" ### 0.183s elapsed time, 0.368s cpu time, 0.000s GC time Loading theory "CoreC++.ClassRel" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects" via "CoreC++.SubObj") Proofs for inductive predicate(s) "subclsRp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "subclsSp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "subcls1p" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "CoreC++.ClassRel" ### 0.398s elapsed time, 0.800s cpu time, 0.000s GC time Loading theory "CoreC++.SubObj" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions" via "CoreC++.Objects") ### Ignoring duplicate safe elimination (elim!) ### \\x\?A. ?P x; ### \x. \x \ ?A; ?P x\ \ ?Q\ ### \ ?Q Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" Proofs for inductive predicate(s) "Subobjs\<^sub>R" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "Subobjs" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "casts_to" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "Casts_to" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "leq_path1p" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Ambiguous input (line 717 of "~~/afp/thys/CoreC++/SubObj.thy") produces 3 parse trees: ### ("\<^const>Pure.eq" ### ("_applC" ("_position" MinimalMethodDefs) ### ("_cargs" ("_position" P) ("_cargs" ("_position" C) ("_position" M)))) ### ("_Coll" ("_pattern" ("_position" Cs) ("_position" mthd)) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("_tuple" ("_position" Cs) ("_tuple_arg" ("_position" mthd))) ### ("_applC" ("_position" MethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_position" C) ("_position" M))))) ### ("_Ball" ("_pattern" ("_position" Cs') ("_position" mthd')) ### ("_applC" ("_position" MethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_position" C) ("_position" M)))) ### ("\<^const>HOL.eq" ### ("\<^const>SubObj.leq_path" ("_position" P) ("_position" C) ### ("_position" Cs') ### ("\<^const>HOL.implies" ("_position" Cs) ("_position" Cs'))) ### ("_position" Cs)))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" MinimalMethodDefs) ### ("_cargs" ("_position" P) ("_cargs" ("_position" C) ("_position" M)))) ### ("_Coll" ("_pattern" ("_position" Cs) ("_position" mthd)) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("_tuple" ("_position" Cs) ("_tuple_arg" ("_position" mthd))) ### ("_applC" ("_position" MethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_position" C) ("_position" M))))) ### ("_Ball" ("_pattern" ("_position" Cs') ("_position" mthd')) ### ("_applC" ("_position" MethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_position" C) ("_position" M)))) ### ("\<^const>SubObj.leq_path" ("_position" P) ("_position" C) ### ("_position" Cs') ### ("\<^const>HOL.implies" ("_position" Cs) ### ("\<^const>HOL.eq" ("_position" Cs') ("_position" Cs)))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" MinimalMethodDefs) ### ("_cargs" ("_position" P) ("_cargs" ("_position" C) ("_position" M)))) ### ("_Coll" ("_pattern" ("_position" Cs) ("_position" mthd)) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("_tuple" ("_position" Cs) ("_tuple_arg" ("_position" mthd))) ### ("_applC" ("_position" MethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_position" C) ("_position" M))))) ### ("_Ball" ("_pattern" ("_position" Cs') ("_position" mthd')) ### ("_applC" ("_position" MethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_position" C) ("_position" M)))) ### ("\<^const>HOL.implies" ### ("\<^const>SubObj.leq_path" ("_position" P) ("_position" C) ### ("_position" Cs') ("_position" Cs)) ### ("\<^const>HOL.eq" ("_position" Cs') ("_position" Cs))))))) ### 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 722 of "~~/afp/thys/CoreC++/SubObj.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ### ("_applC" ("_position" OverriderMethodDefs) ### ("_cargs" ("_position" P) ("_cargs" ("_position" R) ("_position" M)))) ### ("_Coll" ("_pattern" ("_position" Cs) ("_position" mthd)) ### ("\<^const>HOL.Ex_binder" ### ("_idts" ("_position" Cs') ("_position" mthd')) ### ("\<^const>HOL.conj" ### ("\<^const>SubObj.LeastMethodDef" ("_position" P) ### ("_applC" ("_position" ldc) ("_position" R)) ("_position" M) ### ("_position" mthd') ("_position" Cs')) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("_tuple" ("_position" Cs) ("_tuple_arg" ("_position" mthd))) ### ("_applC" ("_position" MinimalMethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_applC" ("_position" mdc) ("_position" R)) ### ("_position" M))))) ### ("\<^const>SubObj.appendPath" ### ("\<^const>SubObj.leq_path" ("_position" P) ### ("_applC" ("_position" mdc) ("_position" R)) ("_position" Cs) ### ("_applC" ("_position" snd) ("_position" R))) ### ("_position" Cs'))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" OverriderMethodDefs) ### ("_cargs" ("_position" P) ("_cargs" ("_position" R) ("_position" M)))) ### ("_Coll" ("_pattern" ("_position" Cs) ("_position" mthd)) ### ("\<^const>HOL.Ex_binder" ### ("_idts" ("_position" Cs') ("_position" mthd')) ### ("\<^const>HOL.conj" ### ("\<^const>SubObj.LeastMethodDef" ("_position" P) ### ("_applC" ("_position" ldc) ("_position" R)) ("_position" M) ### ("_position" mthd') ("_position" Cs')) ### ("\<^const>HOL.conj" ### ("\<^const>Set.member" ### ("_tuple" ("_position" Cs) ("_tuple_arg" ("_position" mthd))) ### ("_applC" ("_position" MinimalMethodDefs) ### ("_cargs" ("_position" P) ### ("_cargs" ("_applC" ("_position" mdc) ("_position" R)) ### ("_position" M))))) ### ("\<^const>SubObj.leq_path" ("_position" P) ### ("_applC" ("_position" mdc) ("_position" R)) ("_position" Cs) ### ("\<^const>SubObj.appendPath" ### ("_applC" ("_position" snd) ("_position" R)) ### ("_position" Cs')))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Proofs for inductive predicate(s) "SelectMethodDef" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "CoreC++.SubObj" ### 2.291s elapsed time, 4.524s cpu time, 0.628s GC time Loading theory "CoreC++.Objects" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax" via "CoreC++.Exceptions") Loading theory "CoreC++.TypeRel" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.WWellForm" via "CoreC++.WellForm") Proofs for inductive predicate(s) "init_obj" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "widen" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "CoreC++.Objects" ### 0.130s elapsed time, 0.260s cpu time, 0.000s GC time Loading theory "CoreC++.Exceptions" (required by "CoreC++.CoreC++" via "CoreC++.Determinism" via "CoreC++.TypeSafe" via "CoreC++.HeapExtension" via "CoreC++.Progress" via "CoreC++.Equivalence" via "CoreC++.BigStep" via "CoreC++.Syntax") ### theory "CoreC++.TypeRel" ### 0.096s elapsed time, 0.192s cpu time, 0.000s GC time ### theory "CoreC++.Exceptions" ### 0.090s elapsed time, 0.180s cpu time, 0.000s GC time isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/CoreC++/outline -o pdf -n outline -t /proof,/ML *** Failed to load theory "CoreC++.State" (unresolved "CoreC++.Exceptions") *** Failed to load theory "CoreC++.Syntax" (unresolved "CoreC++.Exceptions") *** Failed to load theory "CoreC++.BigStep" (unresolved "CoreC++.State", "CoreC++.Syntax") *** Failed to load theory "CoreC++.DefAss" (unresolved "CoreC++.BigStep") *** Failed to load theory "CoreC++.SmallStep" (unresolved "CoreC++.State", "CoreC++.Syntax") *** Failed to load theory "CoreC++.SystemClasses" (unresolved "CoreC++.Exceptions") *** Failed to load theory "CoreC++.WellType" (unresolved "CoreC++.Syntax") *** Failed to load theory "CoreC++.Annotate" (unresolved "CoreC++.WellType") *** Failed to load theory "CoreC++.Execute" (unresolved "CoreC++.BigStep", "CoreC++.WellType") *** Failed to load theory "CoreC++.WellForm" (unresolved "CoreC++.SystemClasses", "CoreC++.WellType") *** Failed to load theory "CoreC++.WellTypeRT" (unresolved "CoreC++.WellType") *** Failed to load theory "CoreC++.Conform" (unresolved "CoreC++.Exceptions", "CoreC++.WellTypeRT") *** Failed to load theory "CoreC++.WWellForm" (unresolved "CoreC++.WellForm") *** Failed to load theory "CoreC++.CWellForm" (unresolved "CoreC++.DefAss", "CoreC++.WWellForm", "CoreC++.WellForm", "CoreC++.WellTypeRT") *** Failed to load theory "CoreC++.Equivalence" (unresolved "CoreC++.BigStep", "CoreC++.SmallStep", "CoreC++.WWellForm") *** Failed to load theory "CoreC++.Progress" (unresolved "CoreC++.Conform", "CoreC++.DefAss", "CoreC++.Equivalence") *** Failed to load theory "CoreC++.HeapExtension" (unresolved "CoreC++.Progress") *** Failed to load theory "CoreC++.TypeSafe" (unresolved "CoreC++.CWellForm", "CoreC++.HeapExtension") *** Failed to load theory "CoreC++.Determinism" (unresolved "CoreC++.TypeSafe") *** Failed to load theory "CoreC++.CoreC++" (unresolved "CoreC++.Annotate", "CoreC++.Determinism", "CoreC++.Execute") *** Type unification failed: Clash of types "_ set" and "_ \ _" *** *** Type error in application: incompatible operand type *** *** Operator: fun_upd :: *** (??'a \ ??'b) *** \ ??'a *** \ ??'b \ ??'a \ ??'b *** Operand: {} :: ??'c set *** *** Coercion Inference: *** *** Local coercion insertion on the operand failed: *** No coercion known for type constructors: "set" and "fun" *** At command "definition" (line 30 of "~~/afp/thys/CoreC++/Exceptions.thy")