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 
print_locale! semi thm semi_def


63 


64 
locale lgrp = semi +


65 
fixes one and inv


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


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


68 
print_locale! lgrp thm lgrp_def lgrp_axioms_def


69 


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


71 
fixes zero and neg


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


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


74 
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def


75 


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


77 
print_locale! rev_lgrp thm rev_lgrp_def


78 


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


80 
print_locale! hom thm hom_def


81 


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


83 
print_locale! perturbation thm perturbation_def


84 


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


86 
print_locale! pert_hom thm pert_hom_def


87 


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


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


90 
print_locale! pert_hom' thm pert_hom'_def


91 


92 

28881

93 
text {* Syntax declarations *}

28873

94 


95 
locale logic =


96 
fixes land (infixl "&&" 55)


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


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


99 
and notnot: " ( x) = x"


100 
begin


101 


102 
definition lor (infixl "" 50) where


103 
"x  y = ( x &&  y)"


104 


105 
end


106 
print_locale! logic


107 


108 
locale use_decl = logic + semi "op "


109 
print_locale! use_decl thm use_decl_def


110 

28881

111 


112 
text {* Theorem statements *}


113 

28873

114 
lemma (in lgrp) lcancel:


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


116 
proof


117 
assume "x ** y = x ** z"


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


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


120 
qed simp

28881

121 
print_locale! lgrp


122 

28873

123 


124 
locale rgrp = semi +


125 
fixes one and inv


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


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

28881

128 
begin

28873

129 

28881

130 
lemma rcancel:

28873

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


132 
proof


133 
assume "y ** x = z ** x"


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


135 
by (simp add: assoc [symmetric])


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


137 
qed simp


138 


139 
end

28881

140 
print_locale! rgrp


141 

28886

142 


143 
text {* Patterns *}


144 


145 
lemma (in rgrp)


146 
assumes "y ** x = z ** x" (is ?a)


147 
shows "y = z" (is ?t)


148 
proof 


149 
txt {* Weird proof involving patterns from context element and conclusion. *}


150 
{


151 
assume ?a


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


153 
by (simp add: assoc [symmetric])


154 
then have ?t by (simp add: rone rinv)


155 
}


156 
note x = this


157 
show ?t by (rule x [OF `?a`])


158 
qed


159 


160 
lemma


161 
assumes "P <> P" (is "?p <> _")


162 
shows "?p <> ?p"


163 
.


164 

28896

165 


166 
text {* Interpretation between locales: sublocales *}


167 


168 
sublocale lgrp < right: rgrp


169 
print_facts


170 
proof (intro rgrp.intro semi.intro rgrp_axioms.intro)


171 
{


172 
fix x


173 
have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)


174 
then show "x ** one = x" by (simp add: assoc lcancel)


175 
}


176 
note rone = this


177 
{


178 
fix x


179 
have "inv(x) ** x ** inv(x) = inv(x) ** one"


180 
by (simp add: linv lone rone)


181 
then show "x ** inv(x) = one" by (simp add: assoc lcancel)


182 
}


183 
qed (simp add: assoc)


184 


185 
(* effect on printed locale *)


186 


187 
print_locale! lgrp


188 


189 
(* use of derived theorem *)


190 


191 
lemma (in lgrp)


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


193 
apply (rule rcancel)


194 
done


195 


196 
(* circular interpretation *)


197 


198 
sublocale rgrp < left: lgrp


199 
proof (intro lgrp.intro semi.intro lgrp_axioms.intro)


200 
{


201 
fix x


202 
have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)


203 
then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)


204 
}


205 
note lone = this


206 
{


207 
fix x


208 
have "inv(x) ** (x ** inv(x)) = one ** inv(x)"


209 
by (simp add: rinv lone rone)


210 
then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)


211 
}


212 
qed (simp add: assoc)


213 


214 
(* effect on printed locale *)


215 


216 
print_locale! rgrp


217 
print_locale! lgrp


218 

28881

219 
end
