src/FOL/ex/LocaleTest.thy
changeset 33617 bfee47887ca3
parent 33462 ddcf2004e215
child 33671 4b0f2599ed48
child 33835 d6134fb5a49f
equal deleted inserted replaced
33616:69f0a6271825 33617:bfee47887ca3
   451   (* the latter comes through the sublocale relation *)
   451   (* the latter comes through the sublocale relation *)
   452 
   452 
   453 
   453 
   454 subsection {* Interpretation in theory, then sublocale *}
   454 subsection {* Interpretation in theory, then sublocale *}
   455 
   455 
   456 interpretation (* fol: *) logic "op +" "minus"
   456 interpretation fol: logic "op +" "minus"
   457 (* FIXME declaration of qualified names *)
       
   458   by unfold_locales (rule int_assoc int_minus2)+
   457   by unfold_locales (rule int_assoc int_minus2)+
   459 
   458 
   460 locale logic2 =
   459 locale logic2 =
   461   fixes land (infixl "&&" 55)
   460   fixes land (infixl "&&" 55)
   462     and lnot ("-- _" [60] 60)
   461     and lnot ("-- _" [60] 60)
   463   assumes assoc: "(x && y) && z = x && (y && z)"
   462   assumes assoc: "(x && y) && z = x && (y && z)"
   464     and notnot: "-- (-- x) = x"
   463     and notnot: "-- (-- x) = x"
   465 begin
   464 begin
   466 
   465 
   467 (* FIXME interpretation below fails
       
   468 definition lor (infixl "||" 50) where
   466 definition lor (infixl "||" 50) where
   469   "x || y = --(-- x && -- y)"
   467   "x || y = --(-- x && -- y)"
   470 *)
       
   471 
   468 
   472 end
   469 end
   473 
   470 
   474 sublocale logic < two: logic2
   471 sublocale logic < two: logic2
   475   by unfold_locales (rule assoc notnot)+
   472   by unfold_locales (rule assoc notnot)+
   476 
   473 
   477 thm two.assoc
   474 thm fol.two.assoc
   478 
   475 
   479 
   476 
   480 subsection {* Declarations and sublocale *}
   477 subsection {* Declarations and sublocale *}
   481 
   478 
   482 locale logic_a = logic
   479 locale logic_a = logic