src/FOL/ex/LocaleTest.thy
changeset 36089 8078d496582c
parent 33837 a406f447abef
child 36091 055934ed89b0
equal deleted inserted replaced
36088:a4369989bc45 36089:8078d496582c
   570 
   570 
   571 thm le.less_thm2  (* mixin applied *)
   571 thm le.less_thm2  (* mixin applied *)
   572 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   572 lemma "gless(x, y) <-> gle(x, y) & x ~= y"
   573   by (rule le.less_thm2)
   573   by (rule le.less_thm2)
   574 
   574 
       
   575 text {* Mixin does not leak to a side branch. *}
       
   576 
       
   577 locale mixin3 = reflexive
       
   578 begin
       
   579 lemmas less_thm3 = less_def
       
   580 end
       
   581 
       
   582 interpretation le: mixin3 gle
       
   583   by unfold_locales
       
   584 
       
   585 thm le.less_thm3  (* mixin not applied *)
       
   586 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
       
   587 
   575 text {* Mixin only available in original context *}
   588 text {* Mixin only available in original context *}
   576 
   589 
   577 (* This section is not finished. *)
   590 locale mixin4_base = reflexive
   578 
   591 
   579 locale mixin3 = mixin le' for le' :: "'a => 'a => o" (infix "\<sqsubseteq>''" 50)
   592 locale mixin4_mixin = mixin4_base
   580 
   593 
   581 lemma (in mixin2) before:
   594 interpretation le: mixin4_mixin gle
   582   "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   595   where "reflexive.less(gle, x, y) <-> gless(x, y)"
   583 proof -
   596 proof -
   584   have "reflexive(gle)" by unfold_locales (rule grefl)
   597   show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
   585   note th = reflexive.less_def[OF this]
   598   note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
   586   then show ?thesis by (simp add: th)
   599   show "reflexive.less(gle, x, y) <-> gless(x, y)"
       
   600     by (simp add: reflexive.less_def[OF reflexive] gless_def)
   587 qed
   601 qed
   588 
   602 
   589 interpretation le': mixin2 gle'
   603 locale mixin4_copy = mixin4_base
   590   apply unfold_locales apply (rule grefl') done
   604 begin
   591 
   605 lemmas less_thm4 = less_def
   592 lemma (in mixin2) after:
   606 end
   593   "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   607 
   594 proof -
   608 locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
   595   have "reflexive(gle)" by unfold_locales (rule grefl)
   609 begin
   596   note th = reflexive.less_def[OF this]
   610 lemmas less_thm4' = less_def
   597   then show ?thesis by (simp add: th)
   611 end
   598 qed
   612 
   599 
   613 interpretation le4: mixin4_combined gle' gle
   600 thm le'.less_def le'.less_thm le'.less_thm2 le'.before le'.after
   614   by unfold_locales (rule grefl')
   601 
   615 
   602 locale combined = le: reflexive le + le': mixin le'
   616 thm le4.less_thm4' (* mixin not applied *)
   603   for le :: "'a => 'a => o" (infixl "\<sqsubseteq>" 50) and le' :: "'a => 'a => o" (infixl "\<sqsubseteq>''" 50)
   617 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   604 
   618   by (rule le4.less_thm4')
   605 interpretation combined gle gle'
       
   606   apply unfold_locales done
       
   607 
       
   608 thm le.less_def le.less_thm le'.less_def le'.less_thm
       
   609 
   619 
   610 
   620 
   611 subsection {* Interpretation in proofs *}
   621 subsection {* Interpretation in proofs *}
   612 
   622 
   613 lemma True
   623 lemma True