src/HOL/ex/LocaleTest2.thy
changeset 22757 d3298d63b7b6
parent 22676 522f4f8aa297
child 23219 87ad6e8a5f2c
equal deleted inserted replaced
22756:b9b78b90ba47 22757:d3298d63b7b6
   107   apply (rule Dint.inv_def) done
   107   apply (rule Dint.inv_def) done
   108 
   108 
   109 interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
   109 interpretation Dclass: Dmonoid ["op +" "0::'a::ab_group_add"]
   110   where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
   110   where "Dmonoid.inv (op +) (0::'a::ab_group_add)" = "uminus"
   111 proof -
   111 proof -
   112   show "Dmonoid (op +) (0::'b::ab_group_add)" by unfold_locales auto
   112   show "Dmonoid (op +) (0::'a::ab_group_add)" by unfold_locales auto
   113   note Dclass = this (* should have this as an assumption in further goals *)
   113   note Dclass = this (* should have this as an assumption in further goals *)
   114   {
   114   {
   115     fix x
   115     fix x
   116     have "Dmonoid.inv (op +) (0::'b::ab_group_add) x = - x"
   116     have "Dmonoid.inv (op +) (0::'a::ab_group_add) x = - x"
   117       by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
   117       by (auto simp: Dmonoid.inv_def [OF Dclass] equals_zero_I [symmetric])
   118   }
   118   }
   119   then show "Dmonoid.inv (op +) (0::'b::ab_group_add) == uminus"
   119   then show "Dmonoid.inv (op +) (0::'a::ab_group_add) == uminus"
   120     by (rule_tac eq_reflection) (fast intro: ext)
   120     by (rule_tac eq_reflection) (fast intro: ext)
   121 qed
   121 qed
   122 
   122 
   123 interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
   123 interpretation Dclass: Dgrp ["op +" "0::'a::ring"]
   124 apply unfold_locales
   124 apply unfold_locales