Loading theory "Markov_Models.Coinductive_Nat" (required by "Markov_Models.Coinductive" via "Markov_Models.Coinductive_List_Prefix" via "Markov_Models.Coinductive_List") Loading theory "Markov_Models.Gauss_Jordan_Elim_Fun" Found termination order: "(\p. size (snd p)) <*mlex*> {}" ### theory "Markov_Models.Gauss_Jordan_Elim_Fun" ### 0.456s elapsed time, 0.976s cpu time, 0.000s GC time 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 "Markov_Models.Coinductive_Nat" ### 1.243s elapsed time, 2.540s cpu time, 0.000s GC time Loading theory "Markov_Models.Coinductive_List" (required by "Markov_Models.Coinductive" via "Markov_Models.Coinductive_List_Prefix") 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" 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)) \ ### Sublist.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" ### Introduced fixed type variable(s): 'a in "P__" or "xs__" ### Introduced fixed type variable(s): 'a in "P__" or "xs__" ### Introduced fixed type variable(s): 'a in "P__" or "Q__" ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a ### 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 "Markov_Models.Coinductive_List" ### 7.643s elapsed time, 14.988s cpu time, 1.196s GC time Loading theory "Markov_Models.Coinductive_List_Prefix" (required by "Markov_Models.Coinductive") instantiation llist :: (type) order less_eq_llist == less_eq :: 'a llist \ 'a llist \ bool less_llist == less :: 'a llist \ 'a llist \ bool 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 "Markov_Models.Coinductive_List_Prefix" ### 0.486s elapsed time, 0.976s cpu time, 0.000s GC time Loading theory "Markov_Models.Coinductive_Stream" (required by "Markov_Models.Coinductive") consts unfold_stream :: "('a \ 'b) \ ('a \ 'a) \ 'a \ 'b stream" Loading theory "Markov_Models.Quotient_Coinductive_List" (required by "Markov_Models.Coinductive") locale stream_from_llist_setup ### theory "Markov_Models.Coinductive_Stream" ### 1.298s elapsed time, 2.576s cpu time, 0.220s GC time Loading theory "Markov_Models.TLList" (required by "Markov_Models.Coinductive") ### theory "Markov_Models.Quotient_Coinductive_List" ### 0.939s elapsed time, 1.860s cpu time, 0.220s GC time ### Ignoring duplicate rewrite rule: ### class.ccpo lSup op \ (mk_less op \) \ True ### 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 overloading terminal0 \ terminal0 :: ('a, 'b) tllist \ 'b consts unfold_tllist :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'c) \ ('a \ 'a) \ 'a \ ('c, 'b) tllist" consts tllist_of_llist :: "'a llist \ ('a, 'b) tllist" consts llist_of_tllist :: "('a, 'b) tllist \ 'a llist" ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a ### theory "Markov_Models.TLList" ### 3.073s elapsed time, 6.124s cpu time, 0.444s GC time Loading theory "Markov_Models.Quotient_TLList" (required by "Markov_Models.Coinductive") ### Introduced fixed type variable(s): 'b in "xs__" ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### theory "Markov_Models.Quotient_TLList" ### 1.132s elapsed time, 2.264s cpu time, 0.000s GC time Loading theory "Markov_Models.Coinductive" ### theory "Markov_Models.Coinductive" ### 0.981s elapsed time, 1.964s cpu time, 0.000s GC time ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a ### 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" ### 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 ### 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. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Ignoring duplicate introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Metis: Unused theorems: "??.unknown" ### Metis: Unused theorems: "??.unknown" ### Ignoring duplicate rewrite rule: ### tllist_all2 op = op = \ op = Testing conjecture with Quickcheck-random... Quickcheck found a counterexample: xs = LCons a\<^sub>1 LNil Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: xs = LCons a\<^sub>1 LNil Evaluated terms: LNil = LNil Testing conjecture with Quickcheck-narrowing... [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Typerep.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Generated_Code.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Main.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/Main.o ) Linking /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5684412/isabelle_quickcheck_narrowing ... Testing conjecture with Quickcheck-random... Quickcheck found a counterexample: xs = TCons a\<^sub>1 (TNil a\<^sub>1) x = a\<^sub>1 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 Testing conjecture with Quickcheck-narrowing... [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Typerep.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Generated_Code.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Main.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/Main.o ) Linking /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5685762/isabelle_quickcheck_narrowing ... [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Typerep.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Generated_Code.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Main.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/Main.o ) Linking /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686446/isabelle_quickcheck_narrowing ... [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Typerep.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Generated_Code.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Main.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/Main.o ) Linking /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686440/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Typerep.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Generated_Code.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Main.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/Main.o ) Linking /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5686674/isabelle_quickcheck_narrowing ... ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Legacy feature! Old 'def' command -- use 'define' instead [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Typerep.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Typerep.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Generated_Code.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Main.hs, /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/Main.o ) Linking /tmp/isabelle-jenkins/process1218584689194439183/Quickcheck_Narrowing5687684/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. ### 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 ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Introduced fixed type variable(s): 'b in "zs__" ### Legacy feature! Old 'def' command -- use 'define' instead ### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_2" ### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_1" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g Loading theory "Markov_Models.Markov_Models_Auxiliary" (required by "Markov_Models.Markov_Models") class order = preorder + assumes "antisym": "\x y. \x \ y; y \ x\ \ x = y" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### Legacy feature! Old 'def' command -- use 'define' instead consts eexp :: "ereal \ ennreal" ### theory "Markov_Models.Markov_Models_Auxiliary" ### 3.445s elapsed time, 6.140s cpu time, 0.240s GC time Loading theory "Markov_Models.Discrete_Time_Markov_Chain" (required by "Markov_Models.Markov_Models") Loading theory "Markov_Models.Discrete_Time_Markov_Process" (required by "Markov_Models.Markov_Models") locale MC_syntax = fixes K :: "'s \ 's pmf" Proofs for coinductive predicate(s) "enabled" locale discrete_Markov_process = fixes M :: "'a measure" and K :: "'a \ 'a measure" assumes "discrete_Markov_process M K" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... consts force_enabled :: "'s \ 's stream \ 's stream" consts walk :: "'s \ ('s \ 's) stream \ 's stream" locale discrete_Markov_process = fixes M :: "'a measure" and K :: "'a \ 'a measure" assumes "discrete_Markov_process M K" ### theory "Markov_Models.Discrete_Time_Markov_Process" ### 0.631s elapsed time, 1.268s cpu time, 0.000s GC time locale MC_with_rewards = fixes K :: "'s \ 's pmf" and \ :: "'s \ 's \ ennreal" and \ :: "'s \ ennreal" assumes "MC_with_rewards \ \" locale MC_pair = fixes K1 :: "'a \ 'a pmf" and K2 :: "'b \ 'b pmf" ### theory "Markov_Models.Discrete_Time_Markov_Chain" ### 1.987s elapsed time, 3.952s cpu time, 0.316s GC time Loading theory "Markov_Models.Classifying_Markov_Chain_States" (required by "Markov_Models.Markov_Models") Proofs for inductive predicate(s) "monoid_closurep" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale MC_syntax = fixes K :: "'s \ 's pmf" Loading theory "Markov_Models.Crowds_Protocol" locale MC_pair = fixes K1 :: "'a \ 'a pmf" and K2 :: "'b \ 'b pmf" locale MC_syntax = fixes K :: "'s \ 's pmf" ### theory "Markov_Models.Classifying_Markov_Chain_States" ### 1.848s elapsed time, 3.704s cpu time, 0.000s GC time Loading theory "Markov_Models.Example_A" locale Crowds_Protocol = fixes J :: "'a set" and C :: "'a set" and p_f :: "real" and p_i :: "'a \ real" assumes "Crowds_Protocol J C p_f p_i" ### theory "Markov_Models.Example_A" ### 1.788s elapsed time, 3.532s cpu time, 0.476s GC time Loading theory "Markov_Models.Example_B" ### theory "Markov_Models.Example_B" ### 0.447s elapsed time, 0.896s cpu time, 0.000s GC time Loading theory "Markov_Models.Gossip_Broadcast" ### theory "Markov_Models.Crowds_Protocol" ### 2.825s elapsed time, 5.612s cpu time, 0.476s GC time Loading theory "Markov_Models.Markov_Decision_Process" (required by "Markov_Models.Markov_Models") locale gossip_broadcast = fixes size :: "nat" and p :: "real" assumes "gossip_broadcast size p" ### theory "Markov_Models.Gossip_Broadcast" ### 1.720s elapsed time, 3.396s cpu time, 0.640s GC time Loading theory "Markov_Models.Trace_Space_Equals_Markov_Processes" (required by "Markov_Models.Markov_Models") Proofs for coinductive predicate(s) "eq_scheduler" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "Markov_Decision_Process.scheduler" found. locale Time_Homogeneous_Discrete_Markov_Process = fixes M :: "'a measure" and S :: "'s set" and X :: "nat \ 'a \ 's" assumes "Time_Homogeneous_Discrete_Markov_Process M S X" Proofs for coinductive predicate(s) "rel_cfg" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... locale Markov_Decision_Process = fixes K :: "'s \ 's pmf set" assumes "Markov_Decision_Process K" Proofs for coinductive predicate(s) "cfg_onp" ### theory "Markov_Models.Trace_Space_Equals_Markov_Processes" ### 0.550s elapsed time, 1.104s cpu time, 0.000s GC time Loading theory "Markov_Models.Zeroconf_Analysis" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... locale Finite_Markov_Decision_Process = fixes K :: "'s \ 's pmf set" and S :: "'s set" assumes "Finite_Markov_Decision_Process K S" ### theory "Markov_Models.Markov_Decision_Process" ### 3.120s elapsed time, 6.204s cpu time, 0.640s GC time Loading theory "Markov_Models.MDP_Reachability_Problem" (required by "Markov_Models.Markov_Models") locale Zeroconf_Analysis = fixes N :: "nat" and p :: "real" and q :: "real" and r :: "real" and e :: "real" assumes "Zeroconf_Analysis p q r e" consts \ :: "zc_state \ zc_state pmf" consts \ :: "zc_state \ zc_state \ real" Proofs for inductive predicate(s) "directed_towardsp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale Reachability_Problem = fixes K :: "'s \ 's pmf set" and S :: "'s set" and S1 :: "'s set" and S2 :: "'s set" assumes "Reachability_Problem K S S1 S2" ### theory "Markov_Models.Zeroconf_Analysis" ### 2.091s elapsed time, 4.140s cpu time, 0.584s GC time Loading theory "Markov_Models.PGCL" ### theory "Markov_Models.MDP_Reachability_Problem" ### 1.584s elapsed time, 3.124s cpu time, 0.584s GC time Loading theory "Markov_Models.MDP_RP_Certification" locale Reachability_Problem = fixes K :: "'s \ 's pmf set" and S :: "'s set" and S1 :: "'s set" and S2 :: "'s set" assumes "Reachability_Problem K S S1 S2" consts wp :: "'s pgcl \ ('s \ ennreal) \ 's \ ennreal" Found termination order: "(\p. size (fst p)) <*mlex*> {}" ### theory "Markov_Models.PGCL" ### 3.906s elapsed time, 7.796s cpu time, 0.552s GC time Loading theory "Markov_Models.Continuous_Time_Markov_Chain" (required by "Markov_Models.Markov_Models") consts merge_at :: "(real \ 'a) stream \ real \ (real \ 'a) stream \ (real \ 'a) stream" locale transition_rates = fixes R :: "'a \ 'a \ real" assumes "transition_rates R" consts lookup :: "'a \ ('b \ 'a) list \ 'b \ 'a" Proofs for inductive predicate(s) "trace_in" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "wf_times" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### theory "Markov_Models.Continuous_Time_Markov_Chain" ### 1.862s elapsed time, 3.688s cpu time, 0.460s GC time Loading theory "Markov_Models.Markov_Models" ### theory "Markov_Models.MDP_RP_Certification" ### 5.564s elapsed time, 11.064s cpu time, 1.012s GC time Loading theory "Markov_Models.PCTL" ### theory "Markov_Models.Markov_Models" ### 1.085s elapsed time, 2.172s cpu time, 0.000s GC time locale Finite_DTMC = fixes K :: "'s \ 's pmf" and S :: "'s set" and \ :: "'s \ real" and \ :: "'s \ 's \ real" assumes "Finite_DTMC K S \ \" ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### countable (set_pmf ?p1) \ True ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### (?P1 \ ?Q1) \ ?R1 \ ?P1 \ ?Q1 \ ?R1 ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### (\x. x \ space ?M \ ?P x) \ ### almost_everywhere ?M ?P ### Legacy feature! Old 'def' command -- use 'define' instead consts bound_until :: "nat \ ('a stream \ bool) \ ('a stream \ bool) \ 'a stream \ bool" consts inrealrel :: "realrel \ 'a \ 'a \ bool" locale Finite_DTMC = fixes K :: "'s \ 's pmf" and S :: "'s set" and \ :: "'s \ real" and \ :: "'s \ 's \ real" assumes "Finite_DTMC K S \ \" consts svalid :: "'s sform \ 's set" pvalid :: "'s pform \ 's stream \ bool" reward :: "'s eform \ 's stream \ ennreal" Found termination order: "(\p. size (fst (snd p))) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" ### Legacy feature! Old 'def' command -- use 'define' instead Found termination order: "size <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### emeasure (T ?s1) (space (stream_space (count_space UNIV))) \ 1 ### theory "Markov_Models.PCTL" ### 9.161s elapsed time, 18.208s cpu time, 1.292s GC time ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### \integrable ?M ?f; integrable ?M ?g\ ### \ integrable ?M (\x. ?f x - ?g x) ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### countable (set_pmf ?p1) \ True ### Rule already declared as introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Rule already declared as introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Ignoring duplicate rewrite rule: ### set_pmf (pair_pmf ?A1 ?B1) \ set_pmf ?A1 \ set_pmf ?B1 ### Rule already declared as introduction (intro) ### (\x. x \ space ?M \ ?P x) \ ### almost_everywhere ?M ?P ### Ignoring duplicate rewrite rule: ### \(0::?'a1) < ?a1; (0::?'a1) < ?b1\ ### \ (0::?'a1) < ?a1 * ?b1 \ True ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### \0 < ?p1; ?p1 < 1\ ### \ set_pmf (bernoulli_pmf ?p1) \ UNIV ### Ignoring duplicate rewrite rule: ### \0 < ?p1; ?p1 < 1\ ### \ set_pmf (bernoulli_pmf ?p1) \ UNIV ### Metis: Unused theorems: "Set.Int_iff" ### Rewrite rule not in simpset: ### op \ \ ### map_fun enn2ereal (map_fun enn2ereal e2ennreal) op \ ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead *** Failed to finish proof (line 37 of "~~/afp/thys/Markov_Models/ex/PCTL.thy"): *** goal (1 subgoal): *** 1. s \ S \ *** (\s'\S. (if s' = s then 1 else 0) * l s') = l s *** At command "by" (line 37 of "~~/afp/thys/Markov_Models/ex/PCTL.thy") ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### \?P ?x; ?x \ ?A\ ### \ \x\?A. ?P x ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Ignoring duplicate rewrite rule: ### e2ennreal 0 \ 0 ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ignoring duplicate rewrite rule: ### (?P1 \