Loading theory "HOL-Analysis.L2_Norm" (required by "HOL-Analysis.Extended_Real_Limits" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") Loading theory "HOL-Analysis.Inner_Product" (required by "HOL-Analysis.Extended_Real_Limits" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector") ### theory "HOL-Analysis.L2_Norm" ### 0.251s elapsed time, 0.572s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Norm_Arith" (required by "HOL-Analysis.Extended_Real_Limits" via "HOL-Analysis.Topology_Euclidean_Space") class real_inner = dist_norm + real_vector + sgn_div_norm + uniformity_dist + open_uniformity + fixes inner :: "'a \ 'a \ real" assumes "inner_commute": "\x y. inner x y = inner y x" and "inner_add_left": "\x y z. inner (x + y) z = inner x z + inner y z" and "inner_scaleR_left": "\r x y. inner (r *\<^sub>R x) y = r * inner x y" and "inner_ge_zero": "\x. 0 \ inner x x" and "inner_eq_zero_iff": "\x. (inner x x = 0) = (x = (0::'a))" and "norm_eq_sqrt_inner": "\x. norm x = sqrt (inner x x)" ### ML warning (line 103 of "~~/src/HOL/Analysis/normarith.ML"): ### Matches are not exhaustive. ### ML warning (line 347 of "~~/src/HOL/Analysis/normarith.ML"): ### Value identifier (instantiate_cterm') has not been referenced. signature NORM_ARITH = sig val norm_arith: Proof.context -> conv val norm_arith_tac: Proof.context -> int -> tactic end structure NormArith: NORM_ARITH ### theory "HOL-Analysis.Norm_Arith" ### 0.425s elapsed time, 0.848s cpu time, 0.000s GC time instantiation real :: real_inner inner_real == inner :: real \ real \ real instantiation complex :: real_inner inner_complex == inner :: complex \ complex \ real ### theory "HOL-Analysis.Inner_Product" ### 1.401s elapsed time, 2.872s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Product_Vector" (required by "HOL-Analysis.Extended_Real_Limits" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra" via "HOL-Analysis.Euclidean_Space") instantiation prod :: (real_vector, real_vector) real_vector scaleR_prod == scaleR :: real \ 'a \ 'b \ 'a \ 'b instantiation prod :: (metric_space, metric_space) dist dist_prod == dist :: 'a \ 'b \ 'a \ 'b \ real instantiation prod :: (metric_space, metric_space) uniformity_dist uniformity_prod == uniformity :: (('a \ 'b) \ 'a \ 'b) filter instantiation prod :: (metric_space, metric_space) metric_space instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector sgn_prod == sgn :: 'a \ 'b \ 'a \ 'b norm_prod == norm :: 'a \ 'b \ real instantiation prod :: (real_inner, real_inner) real_inner inner_prod == inner :: 'a \ 'b \ 'a \ 'b \ real ### theory "HOL-Analysis.Product_Vector" ### 0.726s elapsed time, 1.408s cpu time, 0.180s GC time Loading theory "HOL-Analysis.Euclidean_Space" (required by "HOL-Analysis.Extended_Real_Limits" via "HOL-Analysis.Topology_Euclidean_Space" via "HOL-Analysis.Linear_Algebra") class euclidean_space = real_inner + fixes Basis :: "'a set" assumes "nonempty_Basis": "Basis \ {}" assumes "finite_Basis": "finite Basis" assumes "inner_Basis": "\u v. \u \ Basis; v \ Basis\ \ inner u v = (if u = v then 1 else 0)" assumes "euclidean_all_zero_iff": "\x. (\u\Basis. inner x u = 0) = (x = (0::'a))" instantiation real :: euclidean_space Basis_real == Basis :: real set instantiation complex :: euclidean_space Basis_complex == Basis :: complex set instantiation prod :: (euclidean_space, euclidean_space) euclidean_space Basis_prod == Basis :: ('a \ 'b) set ### theory "HOL-Analysis.Euclidean_Space" ### 1.876s elapsed time, 2.536s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Linear_Algebra" (required by "HOL-Analysis.Extended_Real_Limits" via "HOL-Analysis.Topology_Euclidean_Space") Proofs for inductive predicate(s) "span_induct_alt_helpp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... class real_inner = real_normed_vector + fixes inner :: "'a \ 'a \ real" assumes "inner_commute": "\x y. x \ y = y \ x" and "inner_add_left": "\x y z. (x + y) \ z = x \ z + y \ z" and "inner_scaleR_left": "\r x y. r *\<^sub>R x \ y = r * (x \ y)" and "inner_ge_zero": "\x. 0 \ x \ x" and "inner_eq_zero_iff": "\x. (x \ x = 0) = (x = (0::'a))" and "norm_eq_sqrt_inner": "\x. norm x = sqrt (x \ x)" ### theory "HOL-Analysis.Linear_Algebra" ### 3.673s elapsed time, 6.708s cpu time, 0.460s GC time Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "HOL-Analysis.Extended_Real_Limits") class topological_space = open + assumes "open_UNIV": "open UNIV" assumes "open_Int": "\S T. \open S; open T\ \ open (S \ T)" assumes "open_Union": "\K. Ball K open \ open (\K)" locale countable_basis fixes B :: "'a set set" assumes "countable_basis B" class second_countable_topology = topological_space + assumes "ex_countable_subbasis": "\B. countable B \ open = generate_topology B" ### Ignoring duplicate rewrite rule: ### span UNIV \ UNIV ### Ignoring duplicate rewrite rule: ### span UNIV \ UNIV ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \ (1::?'a1) + of_nat ?m1 class heine_borel = metric_space + assumes "bounded_imp_convergent_subsequence": "\f. bounded (range f) \ \l r. strict_mono r \ (f \ r) \ l" ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### dim UNIV \ DIM(?'a1) ### Ignoring duplicate rewrite rule: ### (0::?'a1) \ span ?S1 \ True ### Ignoring duplicate rewrite rule: ### (0::?'a1) \ span ?S1 \ True ### theory "HOL-Analysis.Topology_Euclidean_Space" ### 8.176s elapsed time, 16.328s cpu time, 0.872s GC time Loading theory "HOL-Analysis.Extended_Real_Limits" ### Ignoring duplicate rewrite rule: ### collinear {?x1, ?y1} \ True ### theory "HOL-Analysis.Extended_Real_Limits" ### 1.590s elapsed time, 3.164s cpu time, 0.344s GC time ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Ignoring duplicate rewrite rule: ### 0 < dist ?x1 ?y1 \ ?x1 \ ?y1 ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate rewrite rule: ### sup ?x1 (- ?x1) \ top ### Rule already declared as introduction (intro) ### countable ?A \ countable (?f ` ?A) ### Rule already declared as introduction (intro) ### \countable ?I; ### \i. i \ ?I \ countable (?A i)\ ### \ countable (Sigma ?I ?A) ### Rule already declared as introduction (intro) ### \countable ?I; ### \i. i \ ?I \ countable (?A i)\ ### \ countable (\i\?I. ?A i) ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \ (1::?'a1) + of_nat ?m1 ### Metis: Unused theorems: "Real_Vector_Spaces.metric_space_class.dist_nz" ### Ignoring duplicate rewrite rule: ### 0 < dist ?x1 ?y1 \ ?x1 \ ?y1 ### Ignoring duplicate rewrite rule: ### 0 < dist ?x1 ?y1 \ ?x1 \ ?y1 Loading theory "Coinductive.Resumption" (required by "Coinductive.Coinductive_Examples") Loading theory "Coinductive.Coinductive_Nat" (required by "Coinductive.Coinductive" via "Coinductive.Coinductive_List_Prefix" via "Coinductive.Coinductive_List") Proofs for coinductive predicate(s) "resumptionp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "enat_setp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... locale co Proofs for coinductive predicate(s) "Le_enatp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### theory "Coinductive.Coinductive_Nat" ### 1.060s elapsed time, 2.168s cpu time, 0.000s GC time Loading theory "Coinductive.Coinductive_List" (required by "Coinductive.Coinductive" via "Coinductive.Coinductive_List_Prefix") consts RESUMPTION_corec_aux :: "nat \ ('e \ ('a, 'b, 'c, 'd, 'e) resumption_corec) \ 'e \ ('c + 'b + 'a, 'd) Old_Datatype.node set" Proofs for coinductive predicate(s) "Eq_RESUMPTION" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### theory "Coinductive.Resumption" ### 1.306s elapsed time, 2.672s cpu time, 0.000s GC time Loading theory "Coinductive.CCPO_Topology" (required by "Coinductive.Coinductive_Examples" via "Coinductive.LList_CCPO_Topology") class ccpo_topology = ccpo + open + assumes "open_ccpo": "\A. open A = (\C. chain C \ C \ {} \ \C \ A \ C \ A \ {})" consts unfold_llist :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'a) \ 'a \ 'b llist" Proofs for inductive predicate(s) "lsetp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "lfinite" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... consts lappend :: "'a llist \ 'a llist \ 'a llist" ### Ignoring duplicate rewrite rule: ### lnull (lappend ?xs1 ?ys1) \ lnull ?xs1 \ lnull ?ys1 Proofs for coinductive predicate(s) "lprefix" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... consts lSup :: "'a llist set \ 'a llist" instantiation set :: (type) ccpo_topology open_set == open :: 'a set set \ bool instantiation enat :: ccpo_topology ### theory "Coinductive.CCPO_Topology" ### 2.346s elapsed time, 4.656s cpu time, 0.412s GC time consts iterates :: "('a \ 'a) \ 'a \ 'a llist" consts llist_of :: "'a list \ 'a llist" consts ltake :: "enat \ 'a llist \ 'a llist" ### Ambiguous input (line 1018 of "~~/afp/thys/Coinductive/Coinductive_List.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" ldrop) ### ("_cargs" ("_position" n) ("_position" xs))) ### ("_case_syntax" ("_position" n) ### ("_case2" ### ("_case1" ("\<^const>Groups.zero_class.zero") ("_position" xs)) ### ("_case2" ### ("_case1" ("_applC" ("_position" eSuc) ("_position" n')) ### ("_case_syntax" ("_position" xs) ### ("_case1" ("_position" LNil) ("_position" LNil)))) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_applC" ("_position" ldrop) ### ("_cargs" ("_position" n') ("_position" xs'))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" ldrop) ### ("_cargs" ("_position" n) ("_position" xs))) ### ("_case_syntax" ("_position" n) ### ("_case2" ### ("_case1" ("\<^const>Groups.zero_class.zero") ("_position" xs)) ### ("_case1" ("_applC" ("_position" eSuc) ("_position" n')) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_applC" ("_position" ldrop) ### ("_cargs" ("_position" n') ("_position" xs'))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. consts ltakeWhile :: "('a \ bool) \ 'a llist \ 'a llist" consts lnth :: "'a llist \ nat \ 'a" consts lzip :: "'a llist \ 'b llist \ ('a \ 'b) llist" Proofs for coinductive predicate(s) "ldistinct" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "llexord" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Ambiguous input (line 1491 of "~~/afp/thys/Coinductive/Coinductive_List.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ("_position" F) ### ("_lambda" ### ("_pttrns" ("_position" ltake) ### ("_pttrns" ("_position" n) ("_position" xs))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs))) ### ("_case_syntax" ("_position" n) ### ("_case2" ### ("_case1" ("\<^const>Groups.zero_class.zero") ### ("_position" LNil)) ### ("_case1" ("_applC" ("_position" eSuc) ("_position" n)) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" ltake) ### ("_cargs" ("_position" n) ("_position" xs))))))))))))) ### ("\<^const>Pure.eq" ("_position" F) ### ("_lambda" ### ("_pttrns" ("_position" ltake) ### ("_pttrns" ("_position" n) ("_position" xs))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs))) ### ("_case_syntax" ("_position" n) ### ("_case1" ("\<^const>Groups.zero_class.zero") ### ("_position" LNil)))) ### ("_case1" ("_applC" ("_position" eSuc) ("_position" n)) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" ltake) ### ("_cargs" ("_position" n) ("_position" xs))))))))))) ### 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: ### lnull (lzip ?xs1 ?ys1) \ lnull ?xs1 \ lnull ?ys1 ### Ambiguous input (line 2468 of "~~/afp/thys/Coinductive/Coinductive_List.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ("_position" F) ### ("_lambda" ### ("_pttrns" ("_position" lzip) ### ("_pattern" ("_position" xs) ("_position" ys))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_case_syntax" ("_position" ys) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ("_position" ys'))) ### ("_applC" ("_position" LCons) ### ("_cargs" ### ("_tuple" ("_position" x) ### ("_tuple_arg" ("_position" y))) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lzip) ### ("_cargs" ("_position" xs') ### ("_position" ys')))))))))))))) ### ("\<^const>Pure.eq" ("_position" F) ### ("_lambda" ### ("_pttrns" ("_position" lzip) ### ("_pattern" ("_position" xs) ("_position" ys))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_case_syntax" ("_position" ys) ### ("_case1" ("_position" LNil) ("_position" LNil)))) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ("_position" ys'))) ### ("_applC" ("_position" LCons) ### ("_cargs" ### ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y))) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lzip) ### ("_cargs" ("_position" xs') ("_position" ys')))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" Proofs for coinductive predicate(s) "lsorted" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Partially applied constant "Sublist.list_emb" on left hand side of equation, in theorem: ### subseq_order.lsorted LNil \ True ### Partially applied constant "Sublist.list_emb" on left hand side of equation, in theorem: ### subseq_order.lsorted (LCons ?x LNil) \ True ### Partially applied constant "Sublist.list_emb" on left hand side of equation, in theorem: ### subseq_order.lsorted (LCons ?x (LCons ?y ?xs)) \ ### subseq ?x ?y \ subseq_order.lsorted (LCons ?y ?xs) ### Partially applied constant "Sublist.sublist" on left hand side of equation, in theorem: ### sublist_order.lsorted LNil \ True ### Partially applied constant "Sublist.sublist" on left hand side of equation, in theorem: ### sublist_order.lsorted (LCons ?x LNil) \ True ### Partially applied constant "Sublist.sublist" on left hand side of equation, in theorem: ### sublist_order.lsorted (LCons ?x (LCons ?y ?xs)) \ ### sublist ?x ?y \ sublist_order.lsorted (LCons ?y ?xs) ### Partially applied constant "Sublist.suffix" on left hand side of equation, in theorem: ### suffix_order.lsorted LNil \ True ### Partially applied constant "Sublist.suffix" on left hand side of equation, in theorem: ### suffix_order.lsorted (LCons ?x LNil) \ True ### Partially applied constant "Sublist.suffix" on left hand side of equation, in theorem: ### suffix_order.lsorted (LCons ?x (LCons ?y ?xs)) \ ### suffix ?x ?y \ suffix_order.lsorted (LCons ?y ?xs) ### Partially applied constant "Sublist.prefix" on left hand side of equation, in theorem: ### prefix_order.lsorted LNil \ True ### Partially applied constant "Sublist.prefix" on left hand side of equation, in theorem: ### prefix_order.lsorted (LCons ?x LNil) \ True ### Partially applied constant "Sublist.prefix" on left hand side of equation, in theorem: ### prefix_order.lsorted (LCons ?x (LCons ?y ?xs)) \ ### prefix ?x ?y \ prefix_order.lsorted (LCons ?y ?xs) class preorder = ord + assumes "less_le_not_le": "\x y. (x < y) = (x \ y \ \ y \ x)" and "order_refl": "\x. x \ x" and "order_trans": "\x y z. \x \ y; y \ z\ \ x \ z" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### Legacy feature! Old 'def' command -- use 'define' instead ### Introduced fixed type variable(s): 'a in "P__" or "xs__" ### Legacy feature! Old 'def' command -- use 'define' instead ### Introduced fixed type variable(s): 'a in "P__" or "xs__" ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Introduced fixed type variable(s): 'a in "P__" or "Q__" ### Ignoring duplicate rewrite rule: ### ((\x. x) \ ?a1) (at ?a1 within ?s1) \ ### True ### Introduced fixed type variable(s): 'a in "xs__" class preorder = ord + assumes "less_le_not_le": "\x y. (x < y) = (x \ y \ \ y \ x)" and "order_refl": "\x. x \ x" and "order_trans": "\x y z. \x \ y; y \ z\ \ x \ z" class monoid_add = semigroup_add + zero + assumes "add_0_left": "\a. (0::'a) + a = a" and "add_0_right": "\a. a + (0::'a) = a" ### theory "Coinductive.Coinductive_List" ### 7.419s elapsed time, 14.120s cpu time, 1.132s GC time Loading theory "Coinductive.Coinductive_List_Prefix" (required by "Coinductive.Coinductive") Testing conjecture with Quickcheck-random... instantiation llist :: (type) order less_eq_llist == less_eq :: 'a llist \ 'a llist \ bool less_llist == less :: 'a llist \ 'a llist \ bool Quickcheck found a counterexample: xs = LCons a\<^sub>1 (LCons a\<^sub>1 LNil) Loading theory "Coinductive.Hamming_Stream" (required by "Coinductive.Coinductive_Examples") instantiation llist :: (type) order_bot bot_llist == bot :: 'a llist instantiation llist :: (type) semilattice_inf inf_llist == inf :: 'a llist \ 'a llist \ 'a llist instantiation llist :: (type) ccpo Sup_llist == Sup :: 'a llist set \ 'a llist ### theory "Coinductive.Coinductive_List_Prefix" ### 0.576s elapsed time, 1.024s cpu time, 0.000s GC time Loading theory "Coinductive.Koenigslemma" (required by "Coinductive.Coinductive_Examples") Proofs for coinductive predicate(s) "pathsp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "reachable_viap" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Coinductive.Koenigslemma" ### 0.374s elapsed time, 0.664s cpu time, 0.000s GC time Loading theory "Coinductive.LMirror" (required by "Coinductive.Coinductive_Examples") class ord = type + fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" consts lmirror_aux :: "'a llist \ 'a llist \ 'a llist" ### Ambiguous input (line 28 of "~~/afp/thys/Coinductive/Examples/Hamming_Stream.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs) ("_position" ys))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_case_syntax" ("_position" ys) ### ("_case1" ("_position" LNil) ("_position" LNil)))) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ("_position" ys'))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ### ("_applC" ("_position" lhd) ("_position" xs)) ### ("_applC" ("_position" lhd) ("_position" ys))) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs') ("_position" ys))))) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ### ("_applC" ("_position" lhd) ("_position" ys)) ### ("_applC" ("_position" lhd) ("_position" xs))) ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs) ("_position" ys'))) ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs') ### ("_position" ys'))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs) ("_position" ys))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_case_syntax" ("_position" ys) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ("_position" ys'))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ### ("_applC" ("_position" lhd) ("_position" xs)) ### ("_applC" ("_position" lhd) ("_position" ys))) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs') ("_position" ys))))) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ### ("_applC" ("_position" lhd) ("_position" ys)) ### ("_applC" ("_position" lhd) ("_position" xs))) ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs) ("_position" ys'))) ### ("_applC" ("_position" lmerge) ### ("_cargs" ("_position" xs') ### ("_position" ys'))))))))))))))) ### 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: ### lnull (lmirror_aux ?acc1 ?xs1) \ lnull ?xs1 \ lnull ?acc1 consts lmerge :: "'a llist \ 'a llist \ 'a llist" ### theory "Coinductive.LMirror" ### 0.237s elapsed time, 0.420s cpu time, 0.000s GC time Loading theory "Coinductive.Lazy_LList" (required by "Coinductive.Lazy_TLList") ### Ignoring duplicate rewrite rule: ### lnull (lmerge ?xs1 ?ys1) \ lnull ?xs1 \ lnull ?ys1 ### Ambiguous input (line 85 of "~~/afp/thys/Coinductive/Examples/Hamming_Stream.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ("_position" F) ### ("_lambda" ### ("_pttrns" ("_position" lmerge) ### ("_pattern" ("_position" xs) ("_position" ys))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_case_syntax" ("_position" ys) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ("_position" ys'))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" x) ### ("_position" y)) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lmerge) ### ("_cargs" ("_position" xs') ("_position" ys)))))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" y) ### ("_position" x)) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lmerge) ### ("_cargs" ("_position" xs) ### ("_position" ys')))))) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lmerge) ### ("_cargs" ("_position" xs') ### ("_position" ys')))))))))))))))) ### ("\<^const>Pure.eq" ("_position" F) ### ("_lambda" ### ("_pttrns" ("_position" lmerge) ### ("_pattern" ("_position" xs) ("_position" ys))) ### ("_case_syntax" ("_position" xs) ### ("_case2" ("_case1" ("_position" LNil) ("_position" LNil)) ### ("_case2" ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ("_position" xs'))) ### ("_case_syntax" ("_position" ys) ### ("_case1" ("_position" LNil) ("_position" LNil)))) ### ("_case1" ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ("_position" ys'))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" x) ### ("_position" y)) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" x) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lmerge) ### ("_cargs" ("_position" xs') ("_position" ys)))))) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" y) ### ("_position" x)) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lmerge) ### ("_cargs" ("_position" xs) ("_position" ys')))))) ### ("_applC" ("_position" LCons) ### ("_cargs" ("_position" y) ### ("_applC" ("_position" curry) ### ("_cargs" ("_position" lmerge) ### ("_cargs" ("_position" xs') ### ("_position" ys')))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### theory "Coinductive.Lazy_LList" ### 0.776s elapsed time, 1.108s cpu time, 0.272s GC time Loading theory "Coinductive.Quotient_Coinductive_List" (required by "Coinductive.Coinductive") ### theory "Coinductive.Hamming_Stream" ### 1.695s elapsed time, 2.700s cpu time, 0.272s GC time Loading theory "Coinductive.TLList" (required by "Coinductive.Coinductive") ### theory "Coinductive.Quotient_Coinductive_List" ### 0.920s elapsed time, 1.544s cpu time, 0.000s GC time Loading theory "Coinductive.Coinductive_Stream" (required by "Coinductive.Coinductive") overloading terminal0 \ terminal0 :: ('a, 'b) tllist \ 'b consts unfold_tllist :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'c) \ ('a \ 'a) \ 'a \ ('c, 'b) tllist" consts unfold_stream :: "('a \ 'b) \ ('a \ 'a) \ 'a \ 'b stream" consts tllist_of_llist :: "'a llist \ ('a, 'b) tllist" consts llist_of_tllist :: "('a, 'b) tllist \ 'a llist" locale stream_from_llist_setup ### theory "Coinductive.Coinductive_Stream" ### 1.294s elapsed time, 2.260s cpu time, 0.000s GC time Loading theory "Coinductive.LList_CCPO_Topology" (required by "Coinductive.Coinductive_Examples") instantiation llist :: (type) ccpo_topology open_llist == open :: 'a llist set \ bool consts edrop :: "enat \ 'a list \ 'a list" ### theory "Coinductive.TLList" ### 3.754s elapsed time, 6.152s cpu time, 0.704s GC time Loading theory "Coinductive.Lazy_TLList" consts up :: "'a \ 'a list \ 'a list" ### theory "Coinductive.Lazy_TLList" ### 0.598s elapsed time, 0.976s cpu time, 0.000s GC time Loading theory "Coinductive.Quotient_TLList" (required by "Coinductive.Coinductive") Found termination order: "case_sum (\p. size_list (nat \ abs) (snd p)) (\p. size_list (nat \ abs) (snd p)) <*mlex*> {}" ### theory "Coinductive.LList_CCPO_Topology" ### 2.716s elapsed time, 4.292s cpu time, 0.704s GC time Loading theory "Coinductive.TLList_CCPO" (required by "Coinductive.Coinductive_Examples" via "Coinductive.TLList_CCPO_Examples") locale tllist_pf fixes b :: "'b" ### theory "Coinductive.TLList_CCPO" ### 0.819s elapsed time, 1.624s cpu time, 0.000s GC time Loading theory "Coinductive.TLList_CCPO_Examples" (required by "Coinductive.Coinductive_Examples") ### theory "Coinductive.Quotient_TLList" ### 1.289s elapsed time, 2.444s cpu time, 0.000s GC time Loading theory "Coinductive.Coinductive" ### Ignoring duplicate rewrite rule: ### \mcont ?luba1 ?orda1 Sup op \ ?f1; ### mcont ?luba1 ?orda1 Sup op \ ?g1\ ### \ ccpo.admissible ?luba1 ?orda1 ### (\x. ?f1 x \ ?g1 x) \ ### True ### theory "Coinductive.TLList_CCPO_Examples" ### 0.169s elapsed time, 0.336s cpu time, 0.000s GC time Loading theory "Coinductive.Coinductive_Examples" ### theory "Coinductive.Coinductive" ### 1.376s elapsed time, 2.500s cpu time, 0.364s GC time Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: xs = LCons a\<^sub>1 LNil Evaluated terms: LNil = LNil Testing conjecture with Quickcheck-narrowing... ### theory "Coinductive.Coinductive_Examples" ### 2.353s elapsed time, 4.116s cpu time, 0.364s GC time [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Typerep.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Generated_Code.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Main.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/Main.o ) Linking /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4285832/isabelle_quickcheck_narrowing ... ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a ### Ignoring duplicate rewrite rule: ### \x\?A1. \ lnull x \ ### lhd (lSup ?A1) \ ### THE x. x \ lhd ` (?A1 \ {xs. \ lnull xs}) ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Typerep.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Generated_Code.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Main.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/Main.o ) Linking /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4287986/isabelle_quickcheck_narrowing ... ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Typerep.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Generated_Code.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Main.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/Main.o ) Linking /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4288070/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. ### Ignoring duplicate rewrite rule: ### ((\x. x) \ ?a1) (at ?a1 within ?s1) \ ### True ### Ignoring duplicate rewrite rule: ### class.ccpo lSup op \ (mk_less op \) \ True ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Introduced fixed type variable(s): 'b in "zs__" ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Legacy feature! Old 'def' command -- use 'define' instead ### Metis: Unused theorems: "Coinductive_List.lappend_llist_of_llist_of" ### Metis: Unused theorems: "Coinductive_List.lfinite_lappend", "Coinductive_List.lfinite_llist_of", "Coinductive_List.list_of_lappend", "Coinductive_List.list_of_llist_of" ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Introduced fixed type variable(s): 'b in "xs__" ### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_2" ### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_1" ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x val zeros = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist val lhd = 0: int val ltl = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist val ltl' = SOME (1, Lazy_llist fn): (int * int Isabelle4316274.Generated_Code.llist) option val ltake = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist val ldrop = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist val list_of = [0, 1]: int list val ltakeWhile = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist val ldropWhile = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist val hd = 0: int val lfilter = Lazy_llist fn: int Isabelle4316274.Generated_Code.llist Testing conjecture with Quickcheck-random... Quickcheck found a counterexample: xs = TCons a\<^sub>1 (TCons a\<^sub>1 (TNil a\<^sub>1)) x = a\<^sub>1 Testing conjecture with Quickcheck-narrowing... Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: xs = TCons a\<^sub>1 (TNil a\<^sub>1) x = a\<^sub>1 Evaluated terms: TNil x = TNil a\<^sub>1 ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### \?r ?a ?b; ?s ?b ?c\ \ (?r OO ?s) ?a ?c ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### \?r ?a ?b; ?s ?b ?c\ \ (?r OO ?s) ?a ?c ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### \?r ?a ?b; ?s ?b ?c\ \ (?r OO ?s) ?a ?c ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### \?r ?a ?b; ?s ?b ?c\ \ (?r OO ?s) ?a ?c ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Rule already declared as introduction (intro) ### \?r ?a ?b; ?s ?b ?c\ \ (?r OO ?s) ?a ?c [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Typerep.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Generated_Code.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Main.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/Main.o ) Linking /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4321004/isabelle_quickcheck_narrowing ... [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Typerep.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Generated_Code.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Main.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/Main.o ) Linking /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4322970/isabelle_quickcheck_narrowing ... [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Typerep.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Generated_Code.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Main.hs, /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/Main.o ) Linking /tmp/isabelle-jenkins/process3597726338088514653/Quickcheck_Narrowing4324734/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. *** exception THM 0 raised (line 328 of "drule.ML"): *** OF: no unifiers *** \closed ?s; \x. isCont ?f x\ *** \ closed (?f -` ?s) *** isCont (\x. (f x, g x)) ?a *** closed {(x, y). llist_all2 ?R x y} *** At command "using" (line 194 of "~~/afp/thys/Coinductive/Examples/LList_CCPO_Topology.thy") ### Ignoring duplicate rewrite rule: ### ((\x. x) \ ?a1) (at ?a1 within ?s1) \ ### True ### Ignoring duplicate rewrite rule: ### ((\x. x) \ ?a1) (at ?a1 within ?s1) \ ### True ### Ignoring duplicate rewrite rule: ### ((\