# [isabelle] How powerful are trans rules?

```Hi,

I’m quite fond of "also ... also ... finally" chains, as they tend to
remove a lot of distracting technicalities from a proof.

When working with HOLCF proofs, I would like to do proofs like this:

begin
fix a b c d f g
have "a ⊑ f ⋅ b" sorry
also have "b ⊑ g ⋅ c" sorry
also have "c ⊑ d" sorry
finally
have "a ⊑ f ⋅ (g ⋅ d)".
end

I currently do that by hard-coding all the variants of the trans rule
that I need:

lemma [trans]:  "a ⊑ f ⋅ b ⟹ b ⊑ c ⟹ a ⊑ f ⋅ c"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]:  "a ⊑ f ⋅ b ⟹ f ⊑ g ⟹ a ⊑ g ⋅ b"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]:  "a ⊑ f ⋅ (g ⋅ b) ⟹ b ⊑ c ⟹ a ⊑ f ⋅ (g ⋅ c)"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]: "a ⊑ f ⋅ b ⋅ c ⋅ d ⟹ b ⊑ b' ⟹ a ⊑ f ⋅ b' ⋅ c ⋅ d"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]:  "a ⊑ f ⋅ b ⋅ c ⋅ d ⟹ c ⊑ c' ⟹ a ⊑ f ⋅ b ⋅ c' ⋅ d"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]:  "a ⊑ f ⋅ (g ⋅ b) ⋅ c ⋅ d ⟹ g ⊑ g' ⟹ a ⊑ f ⋅ (g' ⋅ b) ⋅ c ⋅ d"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)
lemma [trans]:  "a ⊑ f ⋅ b ⋅ (g ⋅ c ⋅ d) ⋅ e ⟹ d ⊑ d' ⟹ a ⊑ f ⋅ b ⋅ (g ⋅ c ⋅ d') ⋅ e"
by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg)

This works, but is rather inflexible and does not scale. And note that
all those trans rules are solved by the same set of rules.

How can I improve that?

One thing I tried was to use

lemma strong_trans[trans]:
"a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y " sorry

This way, the calculation above become

cont (Rep_cfun f) ⟹ cont (λa. f⋅(g⋅a)) ⟹ a ⊑ f⋅(g⋅d)

so using "by simp" instead of "." finishes this. But I find this
annoying (I really like to finish with "finally ?something.").

Is there a way to have the side-condition already checked by "trans" (by
solving it with "intro cont2cont", for example), so that that they never
show up to the user?

That rule also breaks antisymmetry proofs like

begin
fix a b c :: "'a ::cpo"
have "a ⊑ b" sorry
also have "b ⊑ c" sorry
also have "c ⊑ a" sorry
finally
have "a = c".
end

as the calculation at the end will be the unhelpful theorem

cont (λa. a) ⟹ cont (λa. a) ⟹ a ⊑ a.

can I avoid that?

Thanks
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
```

Attachment: signature.asc
Description: This is a digitally signed message part

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