[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:

        notepad
        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

        notepad
        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.