# [isabelle] Proof automation for Types_To_Sets

```Dear list, dear Ondrej and Andrei,

```
I've tried out the new Types_To_Set and I find it very convenient to clean my proofs from unnecessary invariants. However, I am a bit unsatisfied with the level of proof automation. In the ITP2016 paper, it says that the transfer "tool is able to perform the relativization completely automatically". So I was wondering what I am doing wrong.
```
```
My typical use case looks like in the following example. Let's define a while loop operator on subprobability mass functions (import HOL-Probability for this to work) and prove a lemma about probabilistic termination and parametricity of the constants involved:
```
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

```
Now, I would like to add an invariant I on the state of the loop in the termination lemma. At the moment, my proof looks as shown below. I would not call this completely automatic, so I am wondering what I am doing wrong. Can I improve this somehow?
```
```
I use this scheme to add invariants to a bunch of lemmas about loops. At the moment, I just copy-paste the setup script and have it all over the place. Does anyone have an idea how to make this more concise and possibly abstract over it?
```
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'"
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)"
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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.