*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Proof automation for Types_To_Sets*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 18 Nov 2016 15:34:40 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Dear list, dear Ondrej and Andrei,

locale loop_spmf = fixes guard :: "'a â bool" and body :: "'a â 'a spmf" begin partial_function (spmf) while :: "'a â 'a spmf" where "while s = (if guard s then bind_spmf (body s) while else return_spmf s)" lemma termination_0_1: assumes p: "âs. guard s â spmf (map_spmf guard (body s)) False â p" and p_pos: "0 < p" and lossless: "âs. guard s â lossless_spmf (body s)" shows "lossless_spmf (while s)" sorry end context includes lifting_syntax begin lemma lossless_spmf_parametric [transfer_rule]: "(rel_spmf A ===> op =) lossless_spmf lossless_spmf" sorry lemma while_spmf_parametric [transfer_rule]: "((S ===> op =) ===> (S ===> rel_spmf S) ===> S ===> rel_spmf S) loop_spmf.while loop_spmf.while" sorry end lemma loop_spmf_while_cong: "â guard = guard'; âs. guard' s â body s = body' s â â loop_spmf.while guard body = loop_spmf.while guard' body'" sorry

lemma termination_0_1_invar: fixes I :: "'s â bool" assumes p: "âs. â guard s; I s â â spmf (map_spmf guard (body s)) False â p" and p_pos: "0 < p" and lossless: "âs. â guard s; I s â â lossless_spmf (body s)" and invar: "âs s'. â s' â set_spmf (body s); I s; guard s â â I s'" and I: "I s" shows "lossless_spmf (loop_spmf.while guard body s)" including lifting_syntax proof - { assume "â(Rep :: 's' â 's) Abs. type_definition Rep Abs {s. I s}" then obtain Rep :: "'s' â 's" and Abs where td: "type_definition Rep Abs {s. I s}" by blast then interpret td: type_definition Rep Abs "{s. I s}" . def cr â "Îx y. x = Rep y" have [transfer_rule]: "bi_unique cr" "right_total cr" using td cr_def by(rule typedef_bi_unique typedef_right_total)+ have [transfer_domain_rule]: "Domainp cr = I" using type_definition_Domainp[OF td cr_def] by simp def guard' â "(Rep ---> id) guard" have [transfer_rule]: "(cr ===> op =) guard guard'" by(simp add: rel_fun_def cr_def guard'_def) def body1 â "Îs. if guard s then body s else return_pmf None" def body1' â "(Rep ---> map_spmf Abs) body1" have [transfer_rule]: "(cr ===> rel_spmf cr) body1 body1'" by(auto simp add: rel_fun_def body1'_def body1_def cr_def spmf_rel_map td.Rep[simplified] invar td.Abs_inverse intro!: rel_spmf_reflI) def s' â "Abs s" have [transfer_rule]: "cr s s'" by(simp add: s'_def cr_def I td.Abs_inverse) have "âs. guard' s â p â spmf (map_spmf guard' (body1' s)) False" by(transfer fixing: p)(simp add: body1_def p) moreover note p_pos moreover have "âs. guard' s â lossless_spmf (body1' s)" by transfer(simp add: lossless body1_def) ultimately have "lossless_spmf (loop_spmf.while guard' body1' s')" by(rule loop_spmf.termination_0_1_immediate) hence "lossless_spmf (loop_spmf.while guard body1 s)" by transfer } from this[cancel_type_definition] I show ?thesis by(auto cong: loop_spmf_while_cong) qed Thanks, Andreas

- Previous by Date: Re: [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main
- Next by Date: Re: [isabelle] Haskell code generation for Imperative/HOL
- Previous by Thread: Re: [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main
- Next by Thread: Re: [isabelle] Haskell code generation for Imperative/HOL
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list