22657

1 
(* Title: HOL/ex/LocaleTest2.thy


2 
ID: $Id$


3 
Author: Clemens Ballarin


4 
Copyright (c) 2007 by Clemens Ballarin


5 


6 
More regression tests for locales.


7 
Definitions are less natural in FOL, since there is no selection operator.


8 
Hence we do them in HOL, not in the main test suite for locales:


9 
FOL/ex/LocaleTest.thy


10 
*)


11 


12 
header {* Test of Locale Interpretation *}


13 


14 
theory LocaleTest2


15 
imports Main


16 
begin


17 


18 
ML {* set quick_and_dirty *} (* allow for thm command in batch mode *)


19 
ML {* set show_hyps *}


20 
ML {* set show_sorts *}


21 


22 
section {* Interpretation of Defined Concepts *}


23 


24 
text {* Naming convention for global objects: prefixes D and d *}


25 


26 
(* Group example with defined operation inv *)


27 


28 
locale Dsemi =


29 
fixes prod (infixl "**" 65)


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


31 


32 
locale Dmonoid = Dsemi +


33 
fixes one


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


35 
and rone: "x ** one = x"


36 


37 
definition (in Dmonoid)


38 
inv where "inv(x) == THE y. x ** y = one & y ** x = one"


39 


40 
lemma (in Dmonoid) inv_unique:


41 
assumes eq: "y ** x = one" "x ** y' = one"


42 
shows "y = y'"


43 
proof 


44 
from eq have "y = y ** (x ** y')" by (simp add: rone)


45 
also have "... = (y ** x) ** y'" by (simp add: assoc)


46 
also from eq have "... = y'" by (simp add: lone)


47 
finally show ?thesis .


48 
qed


49 


50 
locale Dgrp = Dmonoid +


51 
assumes linv_ex: "EX y. y ** x = one"


52 
and rinv_ex: "EX y. x ** y = one"


53 


54 
lemma (in Dgrp) linv:


55 
"inv x ** x = one"


56 
apply (unfold inv_def)


57 
apply (insert rinv_ex [where x = x])


58 
apply (insert linv_ex [where x = x])


59 
apply (erule exE) apply (erule exE)


60 
apply (rule theI2)


61 
apply rule apply assumption


62 
apply (frule inv_unique, assumption)


63 
apply simp


64 
apply (rule inv_unique)


65 
apply fast+


66 
done


67 


68 
lemma (in Dgrp) rinv:


69 
"x ** inv x = one"


70 
apply (unfold inv_def)


71 
apply (insert rinv_ex [where x = x])


72 
apply (insert linv_ex [where x = x])


73 
apply (erule exE) apply (erule exE)


74 
apply (rule theI2)


75 
apply rule apply assumption


76 
apply (frule inv_unique, assumption)


77 
apply simp


78 
apply (rule inv_unique)


79 
apply fast+


80 
done


81 


82 
lemma (in Dgrp) lcancel:


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


84 
proof


85 
assume "x ** y = x ** z"


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


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


88 
qed simp


89 


90 
interpretation Dint: Dmonoid ["op +" "0::int"]


91 
where "Dmonoid.inv (op +) (0::int)" = "uminus"


92 
proof 


93 
show "Dmonoid (op +) (0::int)" by unfold_locales auto


94 
note Dint = this (* should have this as an assumption in further goals *)


95 
{


96 
fix x


97 
have "Dmonoid.inv (op +) (0::int) x =  x"


98 
by (auto simp: Dmonoid.inv_def [OF Dint])


99 
}


100 
then show "Dmonoid.inv (op +) (0::int) == uminus"


101 
by (rule_tac eq_reflection) (fast intro: ext)


102 
qed


103 


104 
thm Dmonoid.inv_def Dint.inv_def


105 


106 
lemma " x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"


107 
apply (rule Dint.inv_def) done


108 


109 
interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]


110 
where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"


111 
proof 


112 
show "Dmonoid (op +) (0::'b::ab_group_add)" by unfold_locales auto


113 
note Dclass = this (* should have this as an assumption in further goals *)


114 
{


115 
fix x


116 
have "Dmonoid.inv (op +) (0::'b::ab_group_add) x =  x"


117 
by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])


118 
}


119 
then show "Dmonoid.inv (op +) (0::'b::ab_group_add) == uminus"


120 
by (rule_tac eq_reflection) (fast intro: ext)


121 
qed


122 


123 
interpretation Dclass: Dgrp ["op +" "0::'a::ring"]


124 
apply unfold_locales


125 
apply (rule_tac x="x" in exI) apply simp


126 
apply (rule_tac x="x" in exI) apply simp


127 
done


128 


129 
(* Equation for inverse from Dclass: Dmonoid effective. *)


130 


131 
thm Dclass.linv


132 
lemma "x + x = (0::'a::ring)" apply (rule Dclass.linv) done


133 


134 
(* Equations have effect in "subscriptions" *)


135 


136 
(* In the same module *)


137 


138 
lemma (in Dmonoid) trivial:


139 
"inv one = inv one"


140 
by rule


141 


142 
thm Dclass.trivial


143 


144 
(* Inherited: interpretation *)


145 


146 
lemma (in Dgrp) inv_inv:


147 
"inv (inv x) = x"


148 
proof 


149 
have "inv x ** inv (inv x) = inv x ** x"


150 
by (simp add: linv rinv)


151 
then show ?thesis by (simp add: lcancel)


152 
qed


153 


154 
thm Dclass.inv_inv


155 
lemma " ( x) = (x::'a::ring)"


156 
apply (rule Dclass.inv_inv) done


157 


158 
end
