Loading theory "Constructive_Cryptography.More_CryptHOL" (required by "Constructive_Cryptography.Constructive_Cryptography" via "Constructive_Cryptography.Wiring" via "Constructive_Cryptography.Distinguisher" via "Constructive_Cryptography.Random_System" via "Constructive_Cryptography.Converter_Rewrite" via "Constructive_Cryptography.Converter" via "Constructive_Cryptography.Resource") Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" ### Rule already declared as safe introduction (intro!) ### (\x. ?P x) \ \x. ?P x specification relcompp_witness1: (?A OO ?B) (fst ?xy) (snd ?xy) \ ?A (fst ?xy) (relcompp_witness ?A ?B ?xy) relcompp_witness2: (?A OO ?B) (fst ?xy) (snd ?xy) \ ?B (relcompp_witness ?A ?B ?xy) (snd ?xy) Found termination order: "{}" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a specification set_rel_witness_pmf': rel_pmf ?A (fst ?xy) (snd ?xy) \ set_pmf (rel_witness_pmf ?A ?xy) \ {(a, b). ?A a b} map1_rel_witness_pmf': rel_pmf ?A (fst ?xy) (snd ?xy) \ map_pmf fst (rel_witness_pmf ?A ?xy) = fst ?xy map2_rel_witness_pmf': rel_pmf ?A (fst ?xy) (snd ?xy) \ map_pmf snd (rel_witness_pmf ?A ?xy) = snd ?xy ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### \?P ?a; \x. ?P x \ x = ?a\ ### \ (THE x. ?P x) = ?a consts enforce_option :: "('a \ bool) \ 'a option \ 'a option" ### Ambiguous input (line 245 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_option) ### ("\<^const>Orderings.top_class.top")) ### ("_position" id))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_option) ### ("\<^const>Order.top_indexed" ("_indexdefault"))) ### ("_position" id))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 251 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_option) ### ("\<^const>Orderings.bot_class.bot")) ### ("_lambda" ("_idtdummy") ("_position" None)))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_option) ### ("\<^const>Order.bottom_indexed" ("_indexdefault"))) ### ("_lambda" ("_idtdummy") ("_position" None)))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 353 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_spmf) ### ("\<^const>Orderings.top_class.top")) ### ("_position" id))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_spmf) ### ("\<^const>Order.top_indexed" ("_indexdefault"))) ### ("_position" id))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 359 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_spmf) ### ("\<^const>Orderings.bot_class.bot")) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" return_pmf) ("_position" None))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_spmf) ### ("\<^const>Order.bottom_indexed" ("_indexdefault"))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" return_pmf) ("_position" None))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 488 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" integrable) ### ("_cargs" ("_position" M) ("_position" f)))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less" ("_position" r) ### ("\<^const>Order.top_indexed" ("_indexdefault")))))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" integrable) ### ("_cargs" ### ("_applC" ("_position" scale_measure) ### ("_cargs" ("_position" r) ("_position" M))) ### ("_position" f))))) ### ("_bigimpl" ### ("_asms" ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" integrable) ### ("_cargs" ("_position" M) ("_position" f)))) ### ("_asm" ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less" ("_position" r) ### ("\<^const>Orderings.top_class.top"))))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" integrable) ### ("_cargs" ### ("_applC" ("_position" scale_measure) ### ("_cargs" ("_position" r) ("_position" M))) ### ("_position" f))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 493 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less" ("_position" r) ### ("\<^const>Orderings.top_class.top"))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Orderings.ord_class.less" ("_position" r) ### ("\<^const>Order.top_indexed" ("_indexdefault")))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Missing patterns in function definition: ### \vb vc v. rel_witness_generat (IO vb vc, Pure v) = undefined ### \va vb vc. rel_witness_generat (Pure va, IO vb vc) = undefined Found termination order: "{}" instantiation \ :: (type, type) order less_eq_\ == less_eq :: ('a, 'b) \ \ ('a, 'b) \ \ bool less_\ == less :: ('a, 'b) \ \ ('a, 'b) \ \ bool instantiation \ :: (type, type) order_bot bot_\ == bot :: ('a, 'b) \ Proofs for inductive predicate(s) "outsp_gpv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Introduced fixed type variable(s): 'd, 'e, 'f in "gpv__" or "x__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "gpv__" or "x__" Proofs for inductive predicate(s) "pred_gpv'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Ambiguous input (line 1282 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_\_gpv) ### ("_cargs" ("_position" \) ("_position" gpv))) ### ("_applC" ("_position" GPV) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_applC" ("_position" map_generat) ### ("_cargs" ("_position" id) ### ("_cargs" ("_position" id) ### ("_applC" ("\<^const>Fun.comp") ### ("_applC" ("_position" enforce_\_gpv) ### ("_position" \)))))) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_lambda" ("_position" generat) ### ("_case_syntax" ("_position" generat) ### ("_case2" ### ("_case1" ("_applC" ("_position" Pure) ("_position" x)) ### ("_applC" ("_position" Pure) ("_position" x))) ### ("_case1" ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ("_position" rpv))) ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ### ("_lambda" ("_position" input) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" input) ### ("_applC" ("_position" responses_\) ### ("_cargs" ("_position" \) ### ("_position" out)))) ### ("_applC" ("_position" rpv) ### ("_position" input)) ### ("_position" Fail))))))))) ### ("_applC" ("_position" enforce_spmf) ### ("_cargs" ### ("_applC" ("_position" pred_generat) ### ("_cargs" ("\<^const>Orderings.top_class.top") ### ("_cargs" ### ("_lambda" ("_position" x) ### ("\<^const>Set.member" ("_position" x) ### ("_applC" ("_position" outs_\) ### ("_position" \)))) ### ("\<^const>Order.top_indexed" ("_indexdefault"))))) ### ("_applC" ("_position" the_gpv) ### ("_position" gpv))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_\_gpv) ### ("_cargs" ("_position" \) ("_position" gpv))) ### ("_applC" ("_position" GPV) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_applC" ("_position" map_generat) ### ("_cargs" ("_position" id) ### ("_cargs" ("_position" id) ### ("_applC" ("\<^const>Fun.comp") ### ("_applC" ("_position" enforce_\_gpv) ### ("_position" \)))))) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_lambda" ("_position" generat) ### ("_case_syntax" ("_position" generat) ### ("_case2" ### ("_case1" ("_applC" ("_position" Pure) ("_position" x)) ### ("_applC" ("_position" Pure) ("_position" x))) ### ("_case1" ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ("_position" rpv))) ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ### ("_lambda" ("_position" input) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" input) ### ("_applC" ("_position" responses_\) ### ("_cargs" ("_position" \) ### ("_position" out)))) ### ("_applC" ("_position" rpv) ### ("_position" input)) ### ("_position" Fail))))))))) ### ("_applC" ("_position" enforce_spmf) ### ("_cargs" ### ("_applC" ("_position" pred_generat) ### ("_cargs" ### ("\<^const>Order.top_indexed" ("_indexdefault")) ### ("_cargs" ### ("_lambda" ("_position" x) ### ("\<^const>Set.member" ("_position" x) ### ("_applC" ("_position" outs_\) ### ("_position" \)))) ### ("\<^const>Order.top_indexed" ("_indexdefault"))))) ### ("_applC" ("_position" the_gpv) ### ("_position" gpv))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_\_gpv) ### ("_cargs" ("_position" \) ("_position" gpv))) ### ("_applC" ("_position" GPV) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_applC" ("_position" map_generat) ### ("_cargs" ("_position" id) ### ("_cargs" ("_position" id) ### ("_applC" ("\<^const>Fun.comp") ### ("_applC" ("_position" enforce_\_gpv) ### ("_position" \)))))) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_lambda" ("_position" generat) ### ("_case_syntax" ("_position" generat) ### ("_case2" ### ("_case1" ("_applC" ("_position" Pure) ("_position" x)) ### ("_applC" ("_position" Pure) ("_position" x))) ### ("_case1" ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ("_position" rpv))) ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ### ("_lambda" ("_position" input) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" input) ### ("_applC" ("_position" responses_\) ### ("_cargs" ("_position" \) ### ("_position" out)))) ### ("_applC" ("_position" rpv) ### ("_position" input)) ### ("_position" Fail))))))))) ### ("_applC" ("_position" enforce_spmf) ### ("_cargs" ### ("_applC" ("_position" pred_generat) ### ("_cargs" ("\<^const>Orderings.top_class.top") ### ("_cargs" ### ("_lambda" ("_position" x) ### ("\<^const>Set.member" ("_position" x) ### ("_applC" ("_position" outs_\) ### ("_position" \)))) ### ("\<^const>Orderings.top_class.top")))) ### ("_applC" ("_position" the_gpv) ### ("_position" gpv))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" enforce_\_gpv) ### ("_cargs" ("_position" \) ("_position" gpv))) ### ("_applC" ("_position" GPV) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_applC" ("_position" map_generat) ### ("_cargs" ("_position" id) ### ("_cargs" ("_position" id) ### ("_applC" ("\<^const>Fun.comp") ### ("_applC" ("_position" enforce_\_gpv) ### ("_position" \)))))) ### ("_applC" ("_position" map_spmf) ### ("_cargs" ### ("_lambda" ("_position" generat) ### ("_case_syntax" ("_position" generat) ### ("_case2" ### ("_case1" ("_applC" ("_position" Pure) ("_position" x)) ### ("_applC" ("_position" Pure) ("_position" x))) ### ("_case1" ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ("_position" rpv))) ### ("_applC" ("_position" IO) ### ("_cargs" ("_position" out) ### ("_lambda" ("_position" input) ### ("\<^const>HOL.If" ### ("\<^const>Set.member" ("_position" input) ### ("_applC" ("_position" responses_\) ### ("_cargs" ("_position" \) ### ("_position" out)))) ### ("_applC" ("_position" rpv) ### ("_position" input)) ### ("_position" Fail))))))))) ### ("_applC" ("_position" enforce_spmf) ### ("_cargs" ### ("_applC" ("_position" pred_generat) ### ("_cargs" ### ("\<^const>Order.top_indexed" ("_indexdefault")) ### ("_cargs" ### ("_lambda" ("_position" x) ### ("\<^const>Set.member" ("_position" x) ### ("_applC" ("_position" outs_\) ### ("_position" \)))) ### ("\<^const>Orderings.top_class.top")))) ### ("_applC" ("_position" the_gpv) ### ("_position" gpv))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. consts enforce_\_gpv :: "('out, 'in) \ \ ('a, 'out, 'in) gpv \ ('a, 'out, 'in) gpv" locale raw_converter_invariant fixes \ :: "('call, 'ret) \" and \' :: "('call', 'ret') \" and callee :: "'s \ 'call \ ('ret \ 's, 'call', 'ret') gpv" and I :: "'s \ bool" assumes "raw_converter_invariant \ \' callee I" locale raw_converter_invariant fixes \ :: "('call, 'ret) \" and \' :: "('call', 'ret') \" and callee :: "'s \ 'call \ ('ret \ 's, 'call', 'ret') gpv" and I :: "'s \ bool" assumes "raw_converter_invariant \ \' callee I" consts left_gpv :: "('a, 'out, 'in) gpv \ ('a, 'out + 'out', 'in + 'in') gpv" consts right_gpv :: "('a, 'out, 'in) gpv \ ('a, 'out' + 'out, 'in' + 'in) gpv" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g Found termination order: "{}" locale raw_converter_invariant fixes \ :: "('call, 'ret) \" and \' :: "('call', 'ret') \" and callee :: "'s \ 'call \ ('ret \ 's, 'call', 'ret') gpv" and I :: "'s \ bool" assumes "raw_converter_invariant \ \' callee I" locale callee_invariant_on fixes callee :: "'s \ 'a \ ('b \ 's) spmf" and I :: "'s \ bool" and \ :: "('a, 'b) \" assumes "callee_invariant_on callee I \" ### Ambiguous input (line 2193 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" callee_invariant) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ("_position" oracle)) ### ("_lambda" ("_pattern" ("_position" s) ("_position" s')) ### ("_applC" ("_position" I) ("_position" s')))))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" callee_invariant) ### ("_cargs" ("_position" oracle) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ("_pattern" ("_position" s) ("_position" s')) ### ("_applC" ("_position" I) ("_position" s'))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 2197 of "$AFP/Constructive_Cryptography/More_CryptHOL.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" callee_invariant) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ("_position" oracle)) ### ("_lambda" ("_position" s) ### ("_applC" ("_position" I) ### ("_applC" ("_position" snd) ("_position" s))))))) ### ("\<^const>HOL.Trueprop" ### ("_applC" ("_position" callee_invariant) ### ("_cargs" ("_position" oracle) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ("_position" s) ### ("_applC" ("_position" I) ### ("_applC" ("_position" snd) ("_position" s)))))))) ### 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) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g consts mk_lossless_gpv :: "('a, 'b, 'c) gpv \ ('a, 'b, 'c) gpv" ### theory "Constructive_Cryptography.More_CryptHOL" ### 6.192s elapsed time, 20.592s cpu time, 0.376s GC time Loading theory "Constructive_Cryptography.Resource" (required by "Constructive_Cryptography.Constructive_Cryptography" via "Constructive_Cryptography.Wiring" via "Constructive_Cryptography.Distinguisher" via "Constructive_Cryptography.Random_System" via "Constructive_Cryptography.Converter_Rewrite" via "Constructive_Cryptography.Converter") ### Introduced fixed type variable(s): 'g, 'h, 'i, 'j, 'k, 'l in "Aa__" or "Ca__" or "Ra__" or "\'__" or "\__" or "gpv'__" or "gpv__" consts map_resource :: "('a', 'b) resource \ ('a, 'b') resource" Proofs for coinductive predicate(s) "rel_resource" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "lossless_resource" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... consts resource_of_oracle :: "'s \ ('a, 'b) resource" consts parallel_resource :: "('a, 'b) resource \ ('c, 'd) resource \ ('a + 'c, 'b + 'd) resource" Proofs for coinductive predicate(s) "WT_resource" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### theory "Constructive_Cryptography.Resource" ### 3.128s elapsed time, 12.392s cpu time, 0.244s GC time Loading theory "Constructive_Cryptography.Converter" (required by "Constructive_Cryptography.Constructive_Cryptography" via "Constructive_Cryptography.Wiring" via "Constructive_Cryptography.Distinguisher" via "Constructive_Cryptography.Random_System" via "Constructive_Cryptography.Converter_Rewrite") ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g consts map_converter :: "('a', 'b, 'out, 'in') converter \ ('a, 'b', 'out', 'in) converter" ### Rule already declared as introduction (intro) ### \?P ?x; ?x \ ?A\ ### \ \x\?A. ?P x ### Ignoring duplicate safe introduction (intro!) ### expectation_gpv' ?gpv \ expectation_gpv fail \ f ?gpv ### Ignoring duplicate safe introduction (intro!) ### \ \g ?gpv \ \ ### expectation_gpv' ?gpv \ expectation_gpv fail \' f ?gpv ### Ignoring duplicate safe introduction (intro!) ### \ \g gpv \ Proofs for inductive predicate(s) "outsp_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "resultsp_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "rel_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "pred_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Rule already declared as introduction (intro) ### \?P ?x; ?x \ ?A\ ### \ \x\?A. ?P x Proofs for coinductive predicate(s) "WT_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "plossless_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Introduced fixed type variable(s): 'd, 'e, 'f in "B__" or "res1__" or "res2__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "B__" or "res1__" or "res2__" consts converter_of_callee :: "'s \ ('a, 'b, 'out, 'in) converter" consts parallel_converter :: "('a, 'b, 'out, 'in) converter \ ('c, 'd, 'out, 'in) converter \ ('a + 'c, 'b + 'd, 'out, 'in) converter" consts id_converter :: "('a, 'b, 'a, 'b) converter" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g consts parallel_converter2 :: "('a, 'b, 'out, 'in) converter \ ('c, 'd, 'out', 'in') converter \ ('a + 'c, 'b + 'd, 'out + 'out', 'in + 'in') converter" consts left_interface :: "('a, 'b, 'out, 'in) converter \ ('a, 'b, 'out + 'out', 'in + 'in') converter" consts right_interface :: "('a, 'b, 'out, 'in) converter \ ('a, 'b, 'out' + 'out, 'in' + 'in) converter" consts converter_of_resource :: "('a, 'b) resource \ ('a, 'b, 'c, 'd) converter" consts restrict_converter :: "('a, 'b, 'c, 'd) converter \ ('a, 'b, 'c, 'd) converter" consts attach :: "('a, 'b, 'out, 'in) converter \ ('out, 'in) resource \ ('a, 'b) resource" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g consts comp_converter :: "('a, 'b, 'out, 'in) converter \ ('out, 'in, 'out', 'in') converter \ ('a, 'b, 'out', 'in') converter" Proofs for coinductive predicate(s) "interaction_any_bounded_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Ignoring duplicate safe introduction (intro!) ### (\x y. ?P x y \ ?Q x y) \ ?P \ ?Q ### Rule already declared as elimination (elim) ### \?A \ ?B; ?c \ ?A\ ### \ ?c \ ?B ### Rule already declared as elimination (elim) ### \?A \ ?B; ?c \ ?A\ ### \ ?c \ ?B ### Introduced fixed type variable(s): 'j in "gpv__" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### theory "Constructive_Cryptography.Converter" ### 8.607s elapsed time, 32.888s cpu time, 0.860s GC time Loading theory "Constructive_Cryptography.Converter_Rewrite" (required by "Constructive_Cryptography.Constructive_Cryptography" via "Constructive_Cryptography.Wiring" via "Constructive_Cryptography.Distinguisher" via "Constructive_Cryptography.Random_System") ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g Proofs for coinductive predicate(s) "eq_resource_on" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "eq_\_generat" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for coinductive predicate(s) "eq_\_gpv" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### Ignoring duplicate rewrite rule: ### ?y\\\\ \ ?y ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x Proofs for coinductive predicate(s) "eq_\_converter" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... ### theory "Constructive_Cryptography.Converter_Rewrite" ### 1.146s elapsed time, 4.520s cpu time, 0.096s GC time Loading theory "Constructive_Cryptography.Random_System" (required by "Constructive_Cryptography.Constructive_Cryptography" via "Constructive_Cryptography.Wiring" via "Constructive_Cryptography.Distinguisher") ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?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) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Introduced fixed type variable(s): 'e, 'f, 'g in "gpv__" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g Found termination order: "(\p. size_list size (fst (snd (snd p)))) <*mlex*> {}" ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" Proofs for inductive predicate(s) "trace_callee_closure" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... ### Introduced fixed type variable(s): 'g, 'h, 'i, 'j, 'k, 'l in "conv1a__" or "conv2a__" or "x__" Proving the induction rule ... Proving the simplification rules ... ### theory "Constructive_Cryptography.Random_System" ### 0.992s elapsed time, 3.912s cpu time, 0.000s GC time Loading theory "Constructive_Cryptography.Distinguisher" (required by "Constructive_Cryptography.Constructive_Cryptography" via "Constructive_Cryptography.Wiring") ### theory "Constructive_Cryptography.Distinguisher" ### 0.200s elapsed time, 0.724s cpu time, 0.000s GC time Loading theory "Constructive_Cryptography.Wiring" (required by "Constructive_Cryptography.Constructive_Cryptography") ### Ignoring duplicate rewrite rule: ### ?A1 \\<^sub>R ?res1 \ ?res1 \ True ### Ignoring duplicate elimination (elim) ### \?P \ ?Q; ?P ?x ?y; ?Q ?x ?y \ PROP ?W\ ### \ PROP ?W ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Introduced fixed type variable(s): 'e, 'f in "Aa__" or "gpv'__" or "gpv__" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g consts swap_sum :: "'a + 'b \ 'b + 'a" Proofs for inductive predicate(s) "wiring" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### theory "Constructive_Cryptography.Wiring" ### 3.830s elapsed time, 14.768s cpu time, 0.580s GC time Loading theory "Constructive_Cryptography.Constructive_Cryptography" locale constructive_security_aux fixes real_resource :: "nat \ ('a + 'e, 'b + 'f) resource" and ideal_resource :: "nat \ ('c + 'e, 'd + 'f) resource" and sim :: "nat \ ('a, 'b, 'c, 'd) converter" and \_real :: "nat \ ('a, 'b) \" and \_ideal :: "nat \ ('c, 'd) \" and \_common :: "nat \ ('e, 'f) \" and bound :: "nat \ enat" and lossless :: "bool" assumes "constructive_security_aux real_resource ideal_resource sim \_real \_ideal \_common bound lossless" locale constructive_security fixes real_resource :: "nat \ ('a + 'e, 'b + 'f) resource" and ideal_resource :: "nat \ ('c + 'e, 'd + 'f) resource" and sim :: "nat \ ('a, 'b, 'c, 'd) converter" and \_real :: "nat \ ('a, 'b) \" and \_ideal :: "nat \ ('c, 'd) \" and \_common :: "nat \ ('e, 'f) \" and bound :: "nat \ enat" and lossless :: "bool" and w :: "nat \ ('c \ 'a) \ ('b \ 'd)" assumes "constructive_security real_resource ideal_resource sim \_real \_ideal \_common bound lossless w" locale constructive_security2 fixes real_resource :: "nat \ ('a + 'e, 'b + 'f) resource" and ideal_resource :: "nat \ ('c + 'e, 'd + 'f) resource" and sim :: "nat \ ('a, 'b, 'c, 'd) converter" and \_real :: "nat \ ('a, 'b) \" and \_ideal :: "nat \ ('c, 'd) \" and \_common :: "nat \ ('e, 'f) \" and bound :: "nat \ enat" and lossless :: "bool" and w :: "nat \ ('c \ 'a) \ ('b \ 'd)" assumes "constructive_security2 real_resource ideal_resource sim \_real \_ideal \_common bound lossless w" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### theory "Constructive_Cryptography.Constructive_Cryptography" ### 0.607s elapsed time, 2.320s cpu time, 0.000s GC time Loading theory "Constructive_Cryptography.System_Construction" (required by "Constructive_Cryptography.Examples" via "Constructive_Cryptography.Secure_Channel" via "Constructive_Cryptography.One_Time_Pad") locale rorc fixes range :: "'r set" ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C id_converter \ Found termination order: "{}" locale key fixes key_gen :: "'k spmf" Found termination order: "{}" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### \map_\ (inv ?f) (inv ?g) ?\, ### map_\ ?f' ?g' ?\' \\<^sub>C ?conv \; ### inj ?f; surj ?g\ ### \ ?\, ?\' \\<^sub>C ### map_converter ?f ?g ?f' ?g' ?conv \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Rule already declared as introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\' \\<^sub>C ?conv \ \ ### ?\,?\' \\<^sub>C ?conv \ ?conv ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ locale channel fixes side_oracle :: "'m cstate \ 'a \ ('b option \ 'm cstate) spmf" ### Rule already declared as introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ Found termination order: "{}" ### Rule already declared as introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### \?\1.0, ?\2.0 \\<^sub>C ?conv1.0 \; ### ?\1', ?\2' \\<^sub>C ?conv2.0 \\ ### \ ?\1.0 \\<^sub>\ ?\1', ### ?\2.0 \\<^sub>\ ?\2' \\<^sub>C ### ?conv1.0 |\<^sub>= ?conv2.0 \ ### Ignoring duplicate introduction (intro) ### (?\1.0 \\<^sub>\ ?\2.0) \\<^sub>\ ### (?\3.0 \\<^sub>\ ?\4.0), ### (?\1.0 \\<^sub>\ ?\3.0) \\<^sub>\ ### (?\2.0 \\<^sub>\ ?\4.0) \\<^sub>C ### parallel_wiring \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ Found termination order: "{}" locale insec_channel ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ ### Ignoring duplicate introduction (intro) ### ?\, ?\ \\<^sub>C 1\<^sub>C \ Found termination order: "{}" locale auth_channel Found termination order: "{}" Found termination order: "{}" locale sec_channel Found termination order: "{}" locale cipher fixes key_alg :: "'k spmf" and enc_alg :: "'k \ 'm \ 'c spmf" and dec_alg :: "'k \ 'c \ 'm option" locale macode fixes range :: "'r set" and mac_alg :: "'r \ 'm \ 'a spmf" ### theory "Constructive_Cryptography.System_Construction" ### 7.933s elapsed time, 27.040s cpu time, 0.836s GC time Loading theory "Constructive_Cryptography.Message_Authentication_Code" (required by "Constructive_Cryptography.Examples" via "Constructive_Cryptography.Secure_Channel") Loading theory "Constructive_Cryptography.One_Time_Pad" (required by "Constructive_Cryptography.Examples" via "Constructive_Cryptography.Secure_Channel") ### Ambiguous input (line 33 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/One_Time_Pad.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ### ("_applC" ("_position" key_channel_send) ### ("_cargs" ("_position" s) ("_position" m))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" k) ("_position" s)) ### ("_applC" ### ("_applC" ("_position" key.key_oracle) ### ("_applC" ("_position" key) ("_position" \))) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" s)) ### ("\<^const>Product_Type.Unity")))) ### ("_do_cons" ### ("_do_bind" ("_position" c) ### ("_applC" ("_position" enc) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" k) ("_position" m))))) ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_idtdummy") ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.send_oracle)) ### ("_cargs" ("_position" s) ("_position" c)))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" s)))))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" key_channel_send) ### ("_cargs" ("_position" s) ("_position" m))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" k) ("_position" s)) ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" key.key_oracle) ### ("_applC" ("_position" key) ("_position" \)))) ### ("_cargs" ("_position" s) ("\<^const>Product_Type.Unity")))) ### ("_do_cons" ### ("_do_bind" ("_position" c) ### ("_applC" ("_position" enc) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" k) ("_position" m))))) ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_idtdummy") ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.send_oracle)) ### ("_cargs" ("_position" s) ("_position" c)))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" s)))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 41 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/One_Time_Pad.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ### ("_applC" ("_position" key_channel_recv) ### ("_cargs" ("_position" s) ("_position" m))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" c) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle)) ### ("_cargs" ("_position" s) ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" c) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c')) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" k) ("_position" s)) ### ("_applC" ### ("_applC" ("_position" key.key_oracle) ### ("_applC" ("_position" key) ("_position" \))) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" s)) ### ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("_applC" ("_position" dec) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" k) ("_position" c')))) ### ("_tuple_arg" ("_position" s)))))))))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" key_channel_recv) ### ("_cargs" ("_position" s) ("_position" m))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" c) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle)) ### ("_cargs" ("_position" s) ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" c) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s))))) ### ("_case1" ("_applC" ("_position" Some) ("_position" c')) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" k) ("_position" s)) ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" key.key_oracle) ### ("_applC" ("_position" key) ### ("_position" \)))) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("_applC" ("_position" dec) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" k) ("_position" c')))) ### ("_tuple_arg" ("_position" s)))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Proofs for inductive predicate(s) "S" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "{}" ### theory "Constructive_Cryptography.One_Time_Pad" ### 0.730s elapsed time, 2.228s cpu time, 0.000s GC time Found termination order: "{}" ### Ambiguous input (line 58 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy") produces 2 parse trees: ### ("\<^const>Pure.eq" ### ("_applC" ("_position" rorc_channel_send) ### ("_cargs" ("_position" s) ("_position" m))) ### ("\<^const>HOL.If" ### ("_applC" ("_position" fst) ### ("_applC" ("_position" fst) ("_position" s))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_args" ### ("_tuple" ("_position" True) ### ("_tuple_arg" ("\<^const>Product_Type.Unity"))) ### ("_tuple_arg" ("_applC" ("_position" snd) ("_position" s)))))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" r) ("_position" s)) ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ("_position" \)))) ### ("_cargs" ("_applC" ("_position" snd) ("_position" s)) ### ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_idtdummy") ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.send_oracle)) ### ("_cargs" ("_position" s) ### ("_tuple" ("_position" a) ### ("_tuple_arg" ("_position" m)))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_args" ### ("_tuple" ("_position" True) ### ("_tuple_arg" ("\<^const>Product_Type.Unity"))) ### ("_tuple_arg" ("_position" s)))))))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" rorc_channel_send) ### ("_cargs" ("_position" s) ("_position" m))) ### ("\<^const>HOL.If" ### ("_applC" ("_position" fst) ### ("_applC" ("_position" fst) ("_position" s))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_args" ### ("_tuple" ("_position" True) ### ("_tuple_arg" ("\<^const>Product_Type.Unity"))) ### ("_tuple_arg" ("_applC" ("_position" snd) ("_position" s)))))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" r) ("_position" s)) ### ("_applC" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ("_position" \))) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" snd) ("_position" s))) ### ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_idtdummy") ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.send_oracle)) ### ("_cargs" ("_position" s) ### ("_tuple" ("_position" a) ### ("_tuple_arg" ("_position" m)))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_args" ### ("_tuple" ("_position" True) ### ("_tuple_arg" ("\<^const>Product_Type.Unity"))) ### ("_tuple_arg" ("_position" s)))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 68 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy") produces 3 parse trees: ### ("\<^const>Pure.eq" ### ("_applC" ("_position" rorc_channel_recv) ### ("_cargs" ("_position" s) ("_position" q))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" m) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle))) ### ("_cargs" ("_position" s) ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" m) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" r) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ### ("_position" \)))) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" s)) ### ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a') ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" a') ### ("_position" a)) ### ("_applC" ("_position" Some) ("_position" m)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s))))))))))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" rorc_channel_recv) ### ("_cargs" ("_position" s) ("_position" q))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" m) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle))) ### ("_cargs" ("_position" s) ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" m) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" r) ("_position" s)) ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ### ("_position" \))))) ### ("_cargs" ("_position" s) ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a') ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" a') ### ("_position" a)) ### ("_applC" ("_position" Some) ("_position" m)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s))))))))))))))) ### ("\<^const>Pure.eq" ### ("_applC" ("_position" rorc_channel_recv) ### ("_cargs" ("_position" s) ("_position" q))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" m) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle))) ### ("_cargs" ("_position" s) ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" m) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_pattern" ("_position" r) ("_position" s)) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ### ("_position" \))))) ### ("_cargs" ("_position" s) ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a') ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" a') ### ("_position" a)) ### ("_applC" ("_position" Some) ("_position" m)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s))))))))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. Found termination order: "{}" Found termination order: "{}" ### Introduced fixed type variable(s): 'a in "s__" ### Introduced fixed type variable(s): 'a in "s__" Found termination order: "{}" ### Introduced fixed type variable(s): 'a in "s__" Found termination order: "{}" Proofs for inductive predicate(s) "S" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "S'" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Constructive_Cryptography.Message_Authentication_Code" ### 6.821s elapsed time, 26.212s cpu time, 0.796s GC time Loading theory "Constructive_Cryptography.Secure_Channel" (required by "Constructive_Cryptography.Examples") ### theory "Constructive_Cryptography.Secure_Channel" ### 1.150s elapsed time, 4.608s cpu time, 0.000s GC time Loading theory "Constructive_Cryptography.Examples" ### theory "Constructive_Cryptography.Examples" ### 0.091s elapsed time, 0.364s cpu time, 0.000s GC time ### Introduced fixed type variable(s): 'a, 'b, 'c, 'd, 'e, 'f, 'g in "A__" or "B__" or "C__" ### Introduced fixed type variable(s): 'h, 'i, 'j, 'k, 'l in "f__" or "g__" or "h__" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Ambiguous input (line 889 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" ?L) ### ("_applC" ("_position" RES) ### ("_cargs" ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" insec_channel.insec_oracle))) ### ("_applC" ### ("\<^const>Fun.map_fun" ("_position" rprodl) ### ("\<^const>Fun.map_fun" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ("_pttrns" ("_position" s) ("_position" m)) ### ("\<^const>HOL.If" ("_position" s) ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_position" r) ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inl) ### ("_position" m)) ### ("_position" Done)))) ### ("_do_cons" ### ("_do_bind" ("_position" a) ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m)))))) ### ("_do_cons" ### ("_do_bind" ("_idtdummy") ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done)))) ### ("_do_final" ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ### ("_position" \)))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ("_pttrns" ("_position" s) ("_position" q)) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ### ("_pattern" ("_position" amo) ("_position" s')) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" amo) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" a) ### ("_tuple_arg" ("_position" m)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ### ("_pattern" ("_position" r) ("_position" s'')) ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ("_position" \)))) ### ("_cargs" ("_position" s') ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a') ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" a') ("_position" a)) ### ("_applC" ("_position" Some) ("_position" m)) ("_position" None)) ### ("_tuple_arg" ("_position" s'')))))))))))))))))))) ### ("_tuple" ### ("_tuple" ("_position" False) ### ("_tuple_arg" ("\<^const>Product_Type.Unity"))) ### ("_tuple_args" ("_position" Map.empty) ### ("_tuple_arg" ("_position" Void)))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_position" ?L) ### ("_applC" ("_position" RES) ### ("_cargs" ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" insec_channel.insec_oracle))) ### ("_applC" ### ("\<^const>Fun.map_fun" ("_position" rprodl) ### ("\<^const>Fun.map_fun" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ("_pttrns" ("_position" s) ("_position" m)) ### ("\<^const>HOL.If" ("_position" s) ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ("_position" r) ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inl) ### ("_position" m)) ### ("_position" Done)))) ### ("_do_cons" ### ("_do_bind" ("_position" a) ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m)))))) ### ("_do_cons" ### ("_do_bind" ("_idtdummy") ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done)))) ### ("_do_final" ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ### ("_position" \)))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ("_pttrns" ("_position" s) ("_position" q)) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ### ("_pattern" ("_position" amo) ("_position" s')) ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" channel.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity")))) ### ("_do_final" ### ("_case_syntax" ("_position" amo) ### ("_case2" ### ("_case1" ("_position" None) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ### ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" a) ### ("_tuple_arg" ("_position" m)))) ### ("_do_block" ### ("_do_cons" ### ("_do_bind" ### ("_pattern" ("_position" r) ("_position" s'')) ### ("_applC" ### ("_applC" ("_position" rorc.rnd_oracle) ### ("_applC" ("_position" rnd) ("_position" \))) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ("_position" s')) ### ("_position" m)))) ### ("_do_cons" ### ("_do_bind" ("_position" a') ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" r) ("_position" m))))) ### ("_do_final" ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" a') ("_position" a)) ### ("_applC" ("_position" Some) ("_position" m)) ("_position" None)) ### ("_tuple_arg" ("_position" s'')))))))))))))))))))) ### ("_tuple" ### ("_tuple" ("_position" False) ### ("_tuple_arg" ("\<^const>Product_Type.Unity"))) ### ("_tuple_args" ("_position" Map.empty) ### ("_tuple_arg" ("_position" Void)))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Introduced fixed type variable(s): 'a, 'b in "a__" or "b__" ### Introduced fixed type variable(s): 'a in "s__" ### Ambiguous input (line 1190 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res') ("_position" \)) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id))))))) ### ("_position" MAC.INSEC.insec_oracle)))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res') ("_position" \)) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ("_position" snd)) ### ("_position" id)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" MAC.INSEC.insec_oracle))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Introduced fixed type variable(s): 'a, 'b, 'c, 'd, 'e, 'f, 'g, 'h in "conv__" or "f__" or "g__" or "res__" ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Ambiguous input (line 1211 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Message_Authentication_Code.thy") produces 8 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id))))))) ### ("_position" MAC.INSEC.insec_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \)) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ("_position" s')) ### ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_position" extend_state_oracle)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id))))))) ### ("_position" MAC.INSEC.insec_oracle)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \)) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ("_position" s')) ### ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" MAC.INSEC.insec_oracle)))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \)) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ("_position" s')) ### ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_position" extend_state_oracle)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" MAC.INSEC.insec_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \)) ### ("_cargs" ### ("\<^const>Computational_Model.extend_state_oracle" ("_position" s')) ### ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id))))))) ### ("_position" MAC.INSEC.insec_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("_cargs" ("_position" s') ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_position" extend_state_oracle)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id))))))) ### ("_position" MAC.INSEC.insec_oracle)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("_cargs" ("_position" s') ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" MAC.INSEC.insec_oracle)))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("_cargs" ("_position" s') ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" res'') ("_position" \)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_position" extend_state_oracle)) ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" insec_query_of) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ### ("_applC" ("_position" map_option) ### ("_position" snd)) ### ("_position" id)))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" MAC.INSEC.insec_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" rprodl) ### ("_cargs" ### ("_applC" ("_position" map_fun) ### ("_cargs" ("_position" id) ### ("_applC" ("_position" map_spmf) ### ("_applC" ("_position" map_prod) ### ("_cargs" ("_position" id) ### ("_position" lprodr)))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("_applC" ("_position" lift_state_oracle) ### ("_cargs" ("_position" extend_state_oracle) ### ("_applC" ("_position" attach_callee) ### ("_cargs" ### ("_lambda" ### ("_pttrns" ("_position" bs) ("_position" m)) ### ("\<^const>HOL.If" ("_position" bs) ### ("_applC" ("_position" Done) ### ("_tuple" ### ("\<^const>Product_Type.Unity") ("_tuple_arg" ("_position" True)))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ("_applC" ("_position" Inl) ("_position" m)) ("_position" Done))) ### ("_lambda" ("_position" r) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" lift_spmf) ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_applC" ("_position" projl) ("_position" r)) ### ("_position" m))))) ### ("_lambda" ("_position" a) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" Pause) ### ("_cargs" ### ("_applC" ("_position" Inr) ### ("_tuple" ("_position" a) ("_tuple_arg" ("_position" m)))) ### ("_position" Done))) ### ("_lambda" ("_idtdummy") ### ("_applC" ("_position" Done) ### ("_tuple" ("\<^const>Product_Type.Unity") ### ("_tuple_arg" ("_position" True)))))))))))) ### ("\<^const>Computational_Model.plus_oracle" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ### ("_position" \))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.send_oracle))))))) ### ("\<^const>Computational_Model.extend_state_oracle" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_lambda" ### ("_pttrns" ("_position" s) ("_position" q)) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>Computational_Model.extend_state_oracle" ### ("_position" A_CHAN.recv_oracle)) ### ("_cargs" ("_position" s) ### ("\<^const>Product_Type.Unity"))) ### ("_lambda" ("_position" x) ### ("_case_syntax" ("_position" x) ### ("_case2" ### ("_case1" ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ("_position" None) ("_tuple_arg" ("_position" s'))))) ### ("_case1" ### ("_tuple" ### ("_applC" ("_position" Some) ### ("_tuple" ("_position" x1) ("_tuple_arg" ("_position" x2a)))) ### ("_tuple_arg" ("_position" s'))) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ### ("\<^const>More_CryptHOL.extend_state_oracle2" ### ("_applC" ("_position" MAC.RO.rnd_oracle) ("_position" \))) ### ("_cargs" ("_position" s') ("_position" x2a))) ### ("_lambda" ("_pattern" ("_position" x) ("_position" s')) ### ("\<^const>Monad_Syntax.bind" ### ("_applC" ("_position" mac) ### ("_cargs" ("_position" \) ### ("_cargs" ("_position" x) ("_position" x2a)))) ### ("_lambda" ("_position" y) ### ("_applC" ("_position" return_spmf) ### ("_tuple" ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" y) ("_position" x1)) ### ("_applC" ("_position" Some) ("_position" x2a)) ### ("_position" None)) ### ("_tuple_arg" ("_position" s'))))))))))))))))))))))))))) ### 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) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g *** Failed to apply initial proof method (line 122 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy"): *** goal (1 subgoal): *** 1. enat q * 2 \ enat (2 * q) *** At command "by" (line 122 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy") isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/outline -o pdf -n outline -t /proof,/ML *** Failed to apply initial proof method (line 122 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy"): *** goal (1 subgoal): *** 1. enat q * 2 \ enat (2 * q) *** At command "by" (line 122 of "$AFP/Constructive_Cryptography/Examples/Secure_Channel/Secure_Channel.thy")