[isabelle] Calling sublocale A < B in A’s context?



Hi,

I have a pattern in my theories where I have a series of locales, each
refining the previous, e.g.

        
        locale A =
          fixes param :: bool
        begin
          lemma A_lem: "param = param"..
        end
        
        locale B = A + assumes "param = True"
        
and then in a different locale, I instantiate the initial locale and
step-for-step work through the assumptions of the following locales. So
what I’d like to do is something like

        locale C =
          fixes n :: nat
        begin
          (* ... *)
          interpretation A "n = 0".
          (* ... *)
          lemma n: "n = 0" sorry
          interpretation B "n = 0" by (unfold_locales, simp add: n)
          (* ... *)
        end

but (as documented, and quite correctly) now the results from locales A
and B are not available when interpreting C, or even when opening
"context C" again later. So what I have to do instead is:

        locale C =
          fixes n :: nat
        begin
          (* ... *)
        end
        sublocale C < A "n = 0".
        context C begin
          (* ... *)
          lemma n: "n = 0" sorry
        end
        sublocale C < B "n = 0" by (unfold_locales, simp add: n)
        context C begin
          (* ... *)
        end

which I find a bit ugly. Is there a way to declare a sublocale
relationship for the current locale form within that locale?


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.