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])
```