28873

1 
(* Title: FOL/ex/NewLocaleTest.thy


2 
ID: $Id$


3 
Author: Clemens Ballarin, TU Muenchen


4 


5 
Testing environment for locale expressions  experimental.


6 
*)


7 


8 
theory NewLocaleTest


9 
imports NewLocaleSetup


10 
begin


11 


12 
ML_val {* set new_locales *}


13 
ML_val {* set Toplevel.debug *}


14 
ML_val {* set show_hyps *}


15 


16 


17 
typedecl int arities int :: "term"


18 
consts plus :: "int => int => int" (infixl "+" 60)


19 
zero :: int ("0")


20 
minus :: "int => int" (" _")


21 


22 


23 
text {* Inference of parameter types *}


24 


25 
locale param1 = fixes p


26 
print_locale! param1


27 

28881

28 
locale param2 = fixes p :: 'b

28873

29 
print_locale! param2


30 


31 
(*


32 
locale param_top = param2 r for r :: "'b :: {}"


33 
print_locale! param_top


34 
*)


35 


36 
locale param3 = fixes p (infix ".." 50)


37 
print_locale! param3


38 


39 
locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)


40 
print_locale! param4


41 


42 


43 
text {* Incremental type constraints *}


44 


45 
locale constraint1 =


46 
fixes prod (infixl "**" 65)


47 
assumes l_id: "x ** y = x"


48 
assumes assoc: "(x ** y) ** z = x ** (y ** z)"


49 
print_locale! constraint1


50 


51 
locale constraint2 =


52 
fixes p and q


53 
assumes "p = q"


54 
print_locale! constraint2


55 


56 

28881

57 
text {* Inheritance *}

28873

58 


59 
locale semi =


60 
fixes prod (infixl "**" 65)


61 
assumes assoc: "(x ** y) ** z = x ** (y ** z)"


62 
and comm: "x ** y = y ** x"


63 
print_locale! semi thm semi_def


64 


65 
locale lgrp = semi +


66 
fixes one and inv


67 
assumes lone: "one ** x = x"


68 
and linv: "inv(x) ** x = one"


69 
print_locale! lgrp thm lgrp_def lgrp_axioms_def


70 


71 
locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +


72 
fixes zero and neg


73 
assumes lzero: "zero ++ x = x"


74 
and lneg: "neg(x) ++ x = zero"


75 
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def


76 


77 
locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)


78 
print_locale! rev_lgrp thm rev_lgrp_def


79 


80 
locale hom = f: semi f + g: semi g for f and g


81 
print_locale! hom thm hom_def


82 


83 
locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta


84 
print_locale! perturbation thm perturbation_def


85 


86 
locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2


87 
print_locale! pert_hom thm pert_hom_def


88 


89 
text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}


90 
locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2


91 
print_locale! pert_hom' thm pert_hom'_def


92 


93 

28881

94 
text {* Syntax declarations *}

28873

95 


96 
locale logic =


97 
fixes land (infixl "&&" 55)


98 
and lnot (" _" [60] 60)


99 
assumes assoc: "(x && y) && z = x && (y && z)"


100 
and notnot: " ( x) = x"


101 
begin


102 


103 
definition lor (infixl "" 50) where


104 
"x  y = ( x &&  y)"


105 


106 
end


107 
print_locale! logic


108 


109 
locale use_decl = logic + semi "op "


110 
print_locale! use_decl thm use_decl_def


111 

28881

112 


113 
text {* Theorem statements *}


114 

28873

115 
lemma (in lgrp) lcancel:


116 
"x ** y = x ** z <> y = z"


117 
proof


118 
assume "x ** y = x ** z"


119 
then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)


120 
then show "y = z" by (simp add: lone linv)


121 
qed simp

28881

122 
print_locale! lgrp


123 

28873

124 


125 
locale rgrp = semi +


126 
fixes one and inv


127 
assumes rone: "x ** one = x"


128 
and rinv: "x ** inv(x) = one"

28881

129 
begin

28873

130 

28881

131 
lemma rcancel:

28873

132 
"y ** x = z ** x <> y = z"


133 
proof


134 
assume "y ** x = z ** x"


135 
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"


136 
by (simp add: assoc [symmetric])


137 
then show "y = z" by (simp add: rone rinv)


138 
qed simp


139 


140 
end

28881

141 
print_locale! rgrp


142 


143 
end
