src/HOL/Algebra/IntRing.thy
changeset 29237 e90d9d51106b
parent 28823 dcbef866c9e2
child 29242 e190bc2a5399
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:     HOL/Algebra/IntRing.thy
     1.6 -  Id:        $Id$
     1.7    Author:    Stephan Hohe, TU Muenchen
     1.8  *)
     1.9  
    1.10 @@ -97,7 +96,7 @@
    1.11    interpretation needs to be done as early as possible --- that is,
    1.12    with as few assumptions as possible. *}
    1.13  
    1.14 -interpretation int: monoid ["\<Z>"]
    1.15 +interpretation int!: monoid \<Z>
    1.16    where "carrier \<Z> = UNIV"
    1.17      and "mult \<Z> x y = x * y"
    1.18      and "one \<Z> = 1"
    1.19 @@ -105,7 +104,7 @@
    1.20  proof -
    1.21    -- "Specification"
    1.22    show "monoid \<Z>" proof qed (auto simp: int_ring_def)
    1.23 -  then interpret int: monoid ["\<Z>"] .
    1.24 +  then interpret int!: monoid \<Z> .
    1.25  
    1.26    -- "Carrier"
    1.27    show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
    1.28 @@ -117,12 +116,12 @@
    1.29    show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
    1.30  qed
    1.31  
    1.32 -interpretation int: comm_monoid ["\<Z>"]
    1.33 +interpretation int!: comm_monoid \<Z>
    1.34    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    1.35  proof -
    1.36    -- "Specification"
    1.37    show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
    1.38 -  then interpret int: comm_monoid ["\<Z>"] .
    1.39 +  then interpret int!: comm_monoid \<Z> .
    1.40  
    1.41    -- "Operations"
    1.42    { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
    1.43 @@ -140,14 +139,14 @@
    1.44    qed
    1.45  qed
    1.46  
    1.47 -interpretation int: abelian_monoid ["\<Z>"]
    1.48 +interpretation int!: abelian_monoid \<Z>
    1.49    where "zero \<Z> = 0"
    1.50      and "add \<Z> x y = x + y"
    1.51      and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    1.52  proof -
    1.53    -- "Specification"
    1.54    show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
    1.55 -  then interpret int: abelian_monoid ["\<Z>"] .
    1.56 +  then interpret int!: abelian_monoid \<Z> .
    1.57  
    1.58    -- "Operations"
    1.59    { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    1.60 @@ -165,7 +164,7 @@
    1.61    qed
    1.62  qed
    1.63  
    1.64 -interpretation int: abelian_group ["\<Z>"]
    1.65 +interpretation int!: abelian_group \<Z>
    1.66    where "a_inv \<Z> x = - x"
    1.67      and "a_minus \<Z> x y = x - y"
    1.68  proof -
    1.69 @@ -175,7 +174,7 @@
    1.70      show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
    1.71        by (simp add: int_ring_def) arith
    1.72    qed (auto simp: int_ring_def)
    1.73 -  then interpret int: abelian_group ["\<Z>"] .
    1.74 +  then interpret int!: abelian_group \<Z> .
    1.75  
    1.76    -- "Operations"
    1.77    { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    1.78 @@ -188,7 +187,7 @@
    1.79    show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
    1.80  qed
    1.81  
    1.82 -interpretation int: "domain" ["\<Z>"]
    1.83 +interpretation int!: "domain" \<Z>
    1.84    proof qed (auto simp: int_ring_def left_distrib right_distrib)
    1.85  
    1.86  
    1.87 @@ -204,8 +203,8 @@
    1.88    "(True ==> PROP R) == PROP R"
    1.89    by simp_all
    1.90  
    1.91 -interpretation int (* FIXME [unfolded UNIV] *) :
    1.92 -  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.93 +interpretation int! (* FIXME [unfolded UNIV] *) :
    1.94 +  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.95    where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.96      and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.97      and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    1.98 @@ -220,8 +219,8 @@
    1.99      by (simp add: lless_def) auto
   1.100  qed
   1.101  
   1.102 -interpretation int (* FIXME [unfolded UNIV] *) :
   1.103 -  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   1.104 +interpretation int! (* FIXME [unfolded UNIV] *) :
   1.105 +  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   1.106    where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
   1.107      and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
   1.108  proof -
   1.109 @@ -233,7 +232,7 @@
   1.110      apply (simp add: greatest_def Lower_def)
   1.111      apply arith
   1.112      done
   1.113 -  then interpret int: lattice ["?Z"] .
   1.114 +  then interpret int!: lattice "?Z" .
   1.115    show "join ?Z x y = max x y"
   1.116      apply (rule int.joinI)
   1.117      apply (simp_all add: least_def Upper_def)
   1.118 @@ -246,8 +245,8 @@
   1.119      done
   1.120  qed
   1.121  
   1.122 -interpretation int (* [unfolded UNIV] *) :
   1.123 -  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   1.124 +interpretation int! (* [unfolded UNIV] *) :
   1.125 +  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   1.126    proof qed clarsimp
   1.127  
   1.128  
   1.129 @@ -404,7 +403,7 @@
   1.130    assumes zmods: "ZMod m a = ZMod m b"
   1.131    shows "a mod m = b mod m"
   1.132  proof -
   1.133 -  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   1.134 +  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   1.135    from zmods
   1.136        have "b \<in> ZMod m a"
   1.137        unfolding ZMod_def
   1.138 @@ -428,7 +427,7 @@
   1.139  lemma ZMod_mod:
   1.140    shows "ZMod m a = ZMod m (a mod m)"
   1.141  proof -
   1.142 -  interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   1.143 +  interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
   1.144    show ?thesis
   1.145        unfolding ZMod_def
   1.146    apply (rule a_repr_independence'[symmetric])