src/HOL/ex/LocaleTest2.thy
changeset 22657 731622340817
child 22676 522f4f8aa297
equal deleted inserted replaced
22656:13302b2d0948 22657:731622340817
       
     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 Toplevel.debug *}
       
    20 ML {* set show_hyps *}
       
    21 ML {* set show_sorts *}
       
    22 
       
    23 section {* Interpretation of Defined Concepts *}
       
    24 
       
    25 text {* Naming convention for global objects: prefixes D and d *}
       
    26 
       
    27 (* Group example with defined operation inv *)
       
    28 
       
    29 locale Dsemi =
       
    30   fixes prod (infixl "**" 65)
       
    31   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
       
    32 
       
    33 locale Dmonoid = Dsemi +
       
    34   fixes one
       
    35   assumes lone: "one ** x = x"
       
    36     and rone: "x ** one = x"
       
    37 
       
    38 definition (in Dmonoid)
       
    39   inv where "inv(x) == THE y. x ** y = one & y ** x = one"
       
    40 
       
    41 lemma (in Dmonoid) inv_unique:
       
    42   assumes eq: "y ** x = one" "x ** y' = one"
       
    43   shows "y = y'"
       
    44 proof -
       
    45   from eq have "y = y ** (x ** y')" by (simp add: rone)
       
    46   also have "... = (y ** x) ** y'" by (simp add: assoc)
       
    47   also from eq have "... = y'" by (simp add: lone)
       
    48   finally show ?thesis .
       
    49 qed
       
    50 
       
    51 locale Dgrp = Dmonoid +
       
    52   assumes linv_ex: "EX y. y ** x = one"
       
    53     and rinv_ex: "EX y. x ** y = one"
       
    54 
       
    55 lemma (in Dgrp) linv:
       
    56   "inv x ** x = one"
       
    57 apply (unfold inv_def)
       
    58 apply (insert rinv_ex [where x = x])
       
    59 apply (insert linv_ex [where x = x])
       
    60 apply (erule exE) apply (erule exE)
       
    61 apply (rule theI2)
       
    62 apply rule apply assumption
       
    63 apply (frule inv_unique, assumption)
       
    64 apply simp
       
    65 apply (rule inv_unique)
       
    66 apply fast+
       
    67 done
       
    68 
       
    69 lemma (in Dgrp) rinv:
       
    70   "x ** inv x = one"
       
    71 apply (unfold inv_def)
       
    72 apply (insert rinv_ex [where x = x])
       
    73 apply (insert linv_ex [where x = x])
       
    74 apply (erule exE) apply (erule exE)
       
    75 apply (rule theI2)
       
    76 apply rule apply assumption
       
    77 apply (frule inv_unique, assumption)
       
    78 apply simp
       
    79 apply (rule inv_unique)
       
    80 apply fast+
       
    81 done
       
    82 
       
    83 lemma (in Dgrp) lcancel:
       
    84   "x ** y = x ** z <-> y = z"
       
    85 proof
       
    86   assume "x ** y = x ** z"
       
    87   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
       
    88   then show "y = z" by (simp add: lone linv)
       
    89 qed simp
       
    90 
       
    91 interpretation Dint: Dmonoid ["op +" "0::int"]
       
    92   where "Dmonoid.inv (op +) (0::int)" = "uminus"
       
    93 proof -
       
    94   show "Dmonoid (op +) (0::int)" by unfold_locales auto
       
    95   note Dint = this (* should have this as an assumption in further goals *)
       
    96   {
       
    97     fix x
       
    98     have "Dmonoid.inv (op +) (0::int) x = - x"
       
    99       by (auto simp: Dmonoid.inv_def [OF Dint])
       
   100   }
       
   101   then show "Dmonoid.inv (op +) (0::int) == uminus"
       
   102     by (rule_tac eq_reflection) (fast intro: ext)
       
   103 qed
       
   104 
       
   105 thm Dmonoid.inv_def Dint.inv_def
       
   106 
       
   107 lemma "- x \<equiv> THE y. x + y = 0 \<and> y + x = (0::int)"
       
   108   apply (rule Dint.inv_def) done
       
   109 
       
   110 interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
       
   111   where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
       
   112 proof -
       
   113   show "Dmonoid (op +) (0::'b::ab_group_add)" by unfold_locales auto
       
   114   note Dclass = this (* should have this as an assumption in further goals *)
       
   115   {
       
   116     fix x
       
   117     have "Dmonoid.inv (op +) (0::'b::ab_group_add) x = - x"
       
   118       by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
       
   119   }
       
   120   then show "Dmonoid.inv (op +) (0::'b::ab_group_add) == uminus"
       
   121     by (rule_tac eq_reflection) (fast intro: ext)
       
   122 qed
       
   123 
       
   124 interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
       
   125 apply unfold_locales
       
   126 apply (rule_tac x="-x" in exI) apply simp
       
   127 apply (rule_tac x="-x" in exI) apply simp
       
   128 done
       
   129 
       
   130 (* Equation for inverse from Dclass: Dmonoid effective. *)
       
   131 
       
   132 thm Dclass.linv
       
   133 lemma "-x + x = (0::'a::ring)" apply (rule Dclass.linv) done
       
   134 
       
   135 (* Equations have effect in "subscriptions" *)
       
   136 
       
   137 (* In the same module *)
       
   138 
       
   139 lemma (in Dmonoid) trivial:
       
   140   "inv one = inv one"
       
   141   by rule
       
   142 
       
   143 thm Dclass.trivial
       
   144 
       
   145 (* Inherited: interpretation *)
       
   146 
       
   147 lemma (in Dgrp) inv_inv:
       
   148   "inv (inv x) = x"
       
   149 proof -
       
   150   have "inv x ** inv (inv x) = inv x ** x"
       
   151     by (simp add: linv rinv)
       
   152   then show ?thesis by (simp add: lcancel)
       
   153 qed
       
   154 
       
   155 thm Dclass.inv_inv
       
   156 lemma "- (- x) = (x::'a::ring)"
       
   157   apply (rule Dclass.inv_inv) done
       
   158 
       
   159 end