src/HOL/Algebra/UnivPoly.thy
changeset 15596 8665d08085df
parent 15481 fc075ae929e4
child 15696 1da4ce092c0b
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Mar 08 16:02:52 2005 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Mar 09 18:44:52 2005 +0100
     1.3 @@ -369,6 +369,29 @@
     1.4      done
     1.5  qed (simp_all add: R)
     1.6  
     1.7 +(*
     1.8 +Strange phenomenon in Isar:
     1.9 +
    1.10 +theorem (in UP_cring) UP_cring:
    1.11 +  "cring P"
    1.12 +proof (rule cringI)
    1.13 +  show "abelian_group P" proof (rule abelian_groupI)
    1.14 +  fix x y z
    1.15 +  assume "x \<in> carrier P" and "y \<in> carrier P" and "z \<in> carrier P"
    1.16 +  {
    1.17 +  show "x \<oplus>\<^bsub>P\<^esub> y \<in> carrier P" sorry
    1.18 +  next
    1.19 +  show "x \<oplus>\<^bsub>P\<^esub> y \<oplus>\<^bsub>P\<^esub> z = x \<oplus>\<^bsub>P\<^esub> (y \<oplus>\<^bsub>P\<^esub> z)" sorry
    1.20 +  next
    1.21 +  show "x \<oplus>\<^bsub>P\<^esub> y = y \<oplus>\<^bsub>P\<^esub> x" sorry
    1.22 +  next
    1.23 +  show "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> x = x" sorry
    1.24 +  next
    1.25 +  show "\<exists>y\<in>carrier P. y \<oplus>\<^bsub>P\<^esub> x = \<zero>\<^bsub>P\<^esub>" sorry
    1.26 +  next
    1.27 +  show "\<zero>\<^bsub>P\<^esub> \<in> carrier P" sorry  last goal rejected!!!
    1.28 +*)
    1.29 +
    1.30  theorem (in UP_cring) UP_cring:
    1.31    "cring P"
    1.32    by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero