Loading theory "HOL-Library.Case_Converter" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary" via "Coinductive.Coinductive_Stream" via "Coinductive.Coinductive_List" via "HOL-Library.Simps_Case_Conv") Loading theory "HOL-Library.Prefix_Order" (required by "Probabilistic_Noninterference.Interface") Loading theory "Coinductive.Coinductive_Nat" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary" via "Coinductive.Coinductive_Stream" via "Coinductive.Coinductive_List") instantiation list :: (type) order less_eq_list == less_eq :: 'a list \ 'a list \ bool less_list == less :: 'a list \ 'a list \ bool ### theory "HOL-Library.Prefix_Order" ### 0.102s elapsed time, 0.392s cpu time, 0.000s GC time signature CASE_CONVERTER = sig type elimination_strategy val keep_constructor_context: elimination_strategy val replace_by_type: (Proof.context -> string * string -> bool) -> elimination_strategy val to_case: Proof.context -> elimination_strategy -> (string * typ -> int) -> thm list -> thm list option end structure Case_Converter: CASE_CONVERTER ### theory "HOL-Library.Case_Converter" ### 0.398s elapsed time, 0.992s cpu time, 0.000s GC time Loading theory "HOL-Library.Simps_Case_Conv" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary" via "Coinductive.Coinductive_Stream" via "Coinductive.Coinductive_List") signature SIMPS_CASE_CONV = sig val gen_to_simps: Proof.context -> thm list -> thm -> thm list val to_case: Proof.context -> thm list -> thm val to_simps: Proof.context -> thm -> thm list end structure Simps_Case_Conv: SIMPS_CASE_CONV ### theory "HOL-Library.Simps_Case_Conv" ### 0.115s elapsed time, 0.228s 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 "Coinductive.Coinductive_Nat" ### 1.578s elapsed time, 4.264s cpu time, 0.000s GC time Loading theory "Coinductive.Coinductive_List" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary" via "Coinductive.Coinductive_Stream") consts unfold_llist :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'a) \ 'a \ 'b llist" Testing conjecture with Quickcheck-narrowing... 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" 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 consts iterates :: "('a \ 'a) \ 'a \ 'a llist" consts llist_of :: "'a list \ 'a llist" consts ltake :: "enat \ 'a llist \ 'a llist" ### Ambiguous input (line 1019 of "$AFP/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)) ### ("_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'))))))))))) ### ("\<^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'))))))))) ### 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 ... ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a Proofs for coinductive predicate(s) "llexord" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### 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/process4104969405120325033/Quickcheck_Narrowing6795938/Typerep.hs.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Typerep.hs.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Generated_Code.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Main.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/Main.o ) Linking /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6795938/isabelle_quickcheck_narrowing ... ### Ambiguous input (line 1508 of "$AFP/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)) ### ("_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))))))))))) ### ("\<^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))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### 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 ### Ignoring duplicate rewrite rule: ### lnull (lzip ?xs1 ?ys1) \ lnull ?xs1 \ lnull ?ys1 ### Ambiguous input (line 2485 of "$AFP/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)) ### ("_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')))))))))))) ### ("\<^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')))))))))))))) ### 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: ### class.ccpo lSup (\) (mk_less (\)) \ True 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" [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Typerep.hs.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Typerep.hs.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Generated_Code.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Main.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/Main.o ) Linking /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6817886/isabelle_quickcheck_narrowing ... ### 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 ?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): 'a in "xs__" ### Introduced fixed type variable(s): 'b in "zs__" ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x 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" [1 of 4] Compiling Typerep ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Typerep.hs.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Typerep.hs.o ) [2 of 4] Compiling Generated_Code ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Generated_Code.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Generated_Code.o ) [3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Narrowing_Engine.o ) [4 of 4] Compiling Main ( /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Main.hs, /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/Main.o ) Linking /tmp/isabelle-jenkins/process4104969405120325033/Quickcheck_Narrowing6839950/isabelle_quickcheck_narrowing ... ### 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" ### theory "Coinductive.Coinductive_List" ### 9.057s elapsed time, 26.112s cpu time, 1.332s GC time Loading theory "Coinductive.Coinductive_Stream" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary") Quickcheck found no counterexample. ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Introduced fixed type variable(s): 'b in "xs__" consts unfold_stream :: "('a \ 'b) \ ('a \ 'a) \ 'a \ 'b stream" locale stream_from_llist_setup ### theory "Coinductive.Coinductive_Stream" ### 1.450s elapsed time, 5.652s cpu time, 0.000s GC time Loading theory "Markov_Models.Markov_Models_Auxiliary" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain") ### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_2" ### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_1" class order = preorder + assumes "antisym": "\x y. \x \ y; y \ x\ \ x = y" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x consts eexp :: "ereal \ ennreal" ### theory "Markov_Models.Markov_Models_Auxiliary" ### 3.194s elapsed time, 12.184s cpu time, 0.652s GC time Loading theory "Markov_Models.Discrete_Time_Markov_Chain" (required by "Probabilistic_Noninterference.Interface") locale MC_syntax fixes K :: "'s \ 's pmf" Proofs for coinductive predicate(s) "enabled" 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" ### 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 ### Ignoring duplicate rewrite rule: ### 0 \ Suc ` ?A1 \ False locale MC_with_rewards fixes K :: "'s \ 's pmf" and \ :: "'s \ 's \ ennreal" and \ :: "'s \ ennreal" assumes "MC_with_rewards \ \" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g locale MC_pair fixes K1 :: "'a \ 'a pmf" and K2 :: "'b \ 'b pmf" ### theory "Markov_Models.Discrete_Time_Markov_Chain" ### 1.598s elapsed time, 6.320s cpu time, 0.000s GC time Loading theory "Probabilistic_Noninterference.Interface" ### Ignoring duplicate rewrite rule: ### countable (set_pmf ?p1) \ True ### Ignoring duplicate rewrite rule: ### countable (set_pmf ?p1) \ True ### theory "Probabilistic_Noninterference.Interface" ### 2.946s elapsed time, 10.364s cpu time, 0.428s GC time ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Ignoring duplicate rewrite rule: ### (?P1 \ ?Q1) \ ?R1 \ ?P1 \ ?Q1 \ ?R1 ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Ignoring duplicate rewrite rule: ### e2ennreal 0 \ 0 ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### 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 Loading theory "Probabilistic_Noninterference.Language_Semantics" (required by "Probabilistic_Noninterference.Trace_Based" via "Probabilistic_Noninterference.Resumption_Based") ### Metis: Unused theorems: "Groups_Big.comm_monoid_add_class.sum.infinite" ### Metis: Unused theorems: "local.assms_2", "Groups_Big.comm_monoid_add_class.sum.neutral" Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" locale PL fixes aval :: "'atom \ 'state \ 'state" and tval :: "'test \ 'state \ bool" and cval :: "'choice \ 'state \ real" assumes "PL cval" Found termination order: "size <*mlex*> {}" *** Undefined fact: "sum_not_0" (line 702 of "$AFP/Probabilistic_Noninterference/Language_Semantics.thy") *** At command "by" (line 702 of "$AFP/Probabilistic_Noninterference/Language_Semantics.thy") Found termination order: "size <*mlex*> {}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" ### theory "Probabilistic_Noninterference.Language_Semantics" ### 7.461s elapsed time, 22.364s cpu time, 1.012s GC time Loading theory "Probabilistic_Noninterference.Resumption_Based" (required by "Probabilistic_Noninterference.Trace_Based") Proofs for inductive predicate(s) "genp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale PL_Indis fixes aval :: "'atom \ 'state \ 'state" and tval :: "'test \ 'state \ bool" and cval :: "'choice \ 'state \ real" and indis :: "('state \ 'state) set" assumes "PL_Indis cval indis" locale PL_Indis fixes aval :: "'atom \ 'state \ 'state" and tval :: "'test \ 'state \ bool" and cval :: "'choice \ 'state \ real" and indis :: "('state \ 'state) set" assumes "PL_Indis cval indis" Proofs for coinductive predicate(s) "discr" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "siso" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Metis: Unused theorems: "Inductive.coinduct" ### Metis: Unused theorems: "Inductive.coinduct" ### Metis: Unused theorems: "Inductive.complete_lattice_class.gfp_upperbound" Proofs for coinductive predicate(s) "discrCf" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### theory "Probabilistic_Noninterference.Resumption_Based" ### 2.522s elapsed time, 10.020s cpu time, 0.296s GC time Loading theory "Probabilistic_Noninterference.Compositionality" (required by "Probabilistic_Noninterference.Concrete" via "Probabilistic_Noninterference.Syntactic_Criteria") Loading theory "Probabilistic_Noninterference.Trace_Based" locale PL_Indis fixes aval :: "'atom \ 'state \ 'state" and tval :: "'test \ 'state \ bool" and cval :: "'choice \ 'state \ real" and indis :: "('state \ 'state) set" assumes "PL_Indis cval indis" locale PL_Indis fixes aval :: "'atom \ 'state \ 'state" and tval :: "'test \ 'state \ bool" and cval :: "'choice \ 'state \ real" and indis :: "('state \ 'state) set" assumes "PL_Indis cval indis" ### theory "Probabilistic_Noninterference.Trace_Based" ### 1.315s elapsed time, 5.220s cpu time, 0.336s GC time ### theory "Probabilistic_Noninterference.Compositionality" ### 3.081s elapsed time, 12.128s cpu time, 0.616s GC time Loading theory "Probabilistic_Noninterference.Syntactic_Criteria" (required by "Probabilistic_Noninterference.Concrete") locale PL_Indis fixes aval :: "'atom \ 'state \ 'state" and tval :: "'test \ 'state \ bool" and cval :: "'choice \ 'state \ real" and indis :: "('state \ 'state) set" assumes "PL_Indis cval indis" Found termination order: "size <*mlex*> {}" ### Metis: Unused theorems: "Relation.trans_O_subset" ### Metis: Unused theorems: "Relation.sym_conv_converse_eq" ### Metis: Unused theorems: "local.mono_Retr_2" ### Metis: Unused theorems: "local.mono_Retr_1" Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" ### Metis: Unused theorems: "local.assms_2" Found termination order: "size <*mlex*> {}" ### Metis: Unused theorems: "Relation.sym_conv_converse_eq" ### Metis: Unused theorems: "local.mono_Retr_1" ### theory "Probabilistic_Noninterference.Syntactic_Criteria" ### 3.396s elapsed time, 12.244s cpu time, 0.332s GC time Loading theory "Probabilistic_Noninterference.Concrete" instantiation level :: complete_lattice Inf_level == Inf :: level set \ level Sup_level == Sup :: level set \ level bot_level == bot :: level sup_level == sup :: level \ level \ level top_level == top :: level inf_level == inf :: level \ level \ level less_eq_level == less_eq :: level \ level \ bool less_level == less :: level \ level \ bool ### Metis: Unused theorems: "local.brn.simps_1", "local.brn.simps_3", "local.brn.simps_4", "local.brn.simps_5", "local.brn.simps_6", "local.brn.simps_7" ### Metis: Unused theorems: "Set.insertI1", "Set.insert_absorb", "List.insert_code_1", "List.insert_code_2" ### Metis: Unused theorems: "local.brn.simps_1", "local.brn.simps_2", "local.brn.simps_4", "local.brn.simps_5", "local.brn.simps_6", "local.brn.simps_7" ### Metis: Unused theorems: "local.brn.simps_1", "local.brn.simps_2", "local.brn.simps_4", "local.brn.simps_5", "local.brn.simps_6", "local.brn.simps_7" consts sec :: "Concrete.var \ level" Found termination order: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "{}" Found termination order: "{}" ### Ignoring duplicate rewrite rule: ### set_pmf (map_pmf ?f1 ?M1) \ ?f1 ` set_pmf ?M1 Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" ### theory "Probabilistic_Noninterference.Concrete" ### 9.633s elapsed time, 34.724s cpu time, 1.072s GC time ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Ignoring duplicate rewrite rule: ### 0 \ Sigma_Algebra.measure ?M1 ?A1 \ True ### Metis: Unused theorems: "local.indis_trans", "local.indis_sym" ### Metis: Unused theorems: "local.indis_sym" ### Rule already declared as elimination (elim) ### \?ii \ BrnFT ?cl ?dl; ### \n i. ### \n \ theFTOne ?cl ?dl; i < brn (?cl ! n); ### ?ii = brnL ?cl n + i\ ### \ ?phi\ ### \ ?phi ### Ignoring duplicate rewrite rule: ### SC_ZObis Done \ True ### Ignoring duplicate rewrite rule: ### SC_ZObis (Atm ?atm1) \ Example_PL.compatAtm ?atm1 ### Ignoring duplicate rewrite rule: ### SC_ZObis (?c1.1 ;; ?c2.1) \ ### SC_siso ?c1.1 \ SC_ZObis ?c2.1 \ ### SC_ZObis ?c1.1 \ SC_discr ?c2.1 \ SC_Sbis (?c1.1 ;; ?c2.1) ### Ignoring duplicate rewrite rule: ### SC_ZObis (Ch ?ch1 ?c1.1 ?c2.1) \ ### if Example_PL.compatCh ?ch1 then SC_ZObis ?c1.1 \ SC_ZObis ?c2.1 ### else SC_Sbis (Ch ?ch1 ?c1.1 ?c2.1) ### Ignoring duplicate rewrite rule: ### SC_ZObis (While ?tst1 ?c1) \ SC_Sbis (While ?tst1 ?c1) ### Ignoring duplicate rewrite rule: ### SC_ZObis (Par ?cs1) \ SC_Sbis (Par ?cs1) ### Ignoring duplicate rewrite rule: ### SC_ZObis (ParT ?cs1) \ Ball (set ?cs1) SC_Sbis ### Rule already declared as introduction (intro) ### Example_PL.proper Done ### Rule already declared as introduction (intro) ### Example_PL.proper (Atm ?atm) ### Rule already declared as introduction (intro) ### \Example_PL.proper ?c1.0; Example_PL.proper ?c2.0\ ### \ Example_PL.proper (?c1.0 ;; ?c2.0) ### Rule already declared as introduction (intro) ### \Example_PL.proper ?c1.0; Example_PL.proper ?c2.0\ ### \ Example_PL.proper (Ch ?ch ?c1.0 ?c2.0) ### Rule already declared as introduction (intro) ### Example_PL.proper ?c \ Example_PL.proper (While ?tst ?c) ### Rule already declared as introduction (intro) ### Example_PL.properL ?cs \ Example_PL.proper (Par ?cs) ### Rule already declared as introduction (intro) ### Example_PL.properL ?cs \ Example_PL.proper (ParT ?cs) ### Rule already declared as introduction (intro) ### \\c. c \ set ?cs \ Example_PL.proper c; ### ?cs \ []\ ### \ Example_PL.properL ?cs isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/outline -o pdf -n outline -t /proof,/ML *** Undefined fact: "sum_not_0" (line 702 of "$AFP/Probabilistic_Noninterference/Language_Semantics.thy") *** At command "by" (line 702 of "$AFP/Probabilistic_Noninterference/Language_Semantics.thy")