src/HOL/Semiring_Normalization.thy
changeset 36872 6520ba1256a6
parent 36871 3763c349c8c1
child 36873 112e613e8d0b
     1.1 --- a/src/HOL/Semiring_Normalization.thy	Wed May 12 12:31:52 2010 +0200
     1.2 +++ b/src/HOL/Semiring_Normalization.thy	Wed May 12 13:51:22 2010 +0200
     1.3 @@ -57,11 +57,11 @@
     1.4  context comm_semiring_1
     1.5  begin
     1.6  
     1.7 -lemma semiring_ops:
     1.8 +lemma normalizing_semiring_ops:
     1.9    shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)"
    1.10      and "TERM 0" and "TERM 1" .
    1.11  
    1.12 -lemma semiring_rules:
    1.13 +lemma normalizing_semiring_rules:
    1.14    "(a * m) + (b * m) = (a + b) * m"
    1.15    "(a * m) + m = (a + 1) * m"
    1.16    "m + (a * m) = (a + 1) * m"
    1.17 @@ -103,8 +103,8 @@
    1.18  
    1.19  lemmas normalizing_comm_semiring_1_axioms =
    1.20    comm_semiring_1_axioms [normalizer
    1.21 -    semiring ops: semiring_ops
    1.22 -    semiring rules: semiring_rules]
    1.23 +    semiring ops: normalizing_semiring_ops
    1.24 +    semiring rules: normalizing_semiring_rules]
    1.25  
    1.26  declaration
    1.27    {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
    1.28 @@ -114,19 +114,19 @@
    1.29  context comm_ring_1
    1.30  begin
    1.31  
    1.32 -lemma ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
    1.33 +lemma normalizing_ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
    1.34  
    1.35 -lemma ring_rules:
    1.36 +lemma normalizing_ring_rules:
    1.37    "- x = (- 1) * x"
    1.38    "x - y = x + (- y)"
    1.39    by (simp_all add: diff_minus)
    1.40  
    1.41  lemmas normalizing_comm_ring_1_axioms =
    1.42    comm_ring_1_axioms [normalizer
    1.43 -    semiring ops: semiring_ops
    1.44 -    semiring rules: semiring_rules
    1.45 -    ring ops: ring_ops
    1.46 -    ring rules: ring_rules]
    1.47 +    semiring ops: normalizing_semiring_ops
    1.48 +    semiring rules: normalizing_semiring_rules
    1.49 +    ring ops: normalizing_ring_ops
    1.50 +    ring rules: normalizing_ring_rules]
    1.51  
    1.52  declaration
    1.53    {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
    1.54 @@ -137,31 +137,22 @@
    1.55  begin
    1.56  
    1.57  lemma noteq_reduce:
    1.58 -  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
    1.59 -proof-
    1.60 -  have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
    1.61 -  also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
    1.62 -    using add_mult_solve by blast
    1.63 -  finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
    1.64 -    by simp
    1.65 -qed
    1.66 +  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
    1.67 +  by (simp add: add_mult_solve)
    1.68  
    1.69  lemma add_scale_eq_noteq:
    1.70 -  "\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)"
    1.71 -proof(clarify)
    1.72 -  assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d"
    1.73 -    and eq: "b + (r * c) = b + (r * d)"
    1.74 +  "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
    1.75 +proof (rule notI)
    1.76 +  assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
    1.77 +    and eq: "a + (r * c) = b + (r * d)"
    1.78    have "(0 * d) + (r * c) = (0 * c) + (r * d)"
    1.79 -    using add_imp_eq eq mult_zero_left by simp
    1.80 -  thus "False" using add_mult_solve[of 0 d] nz cnd by simp
    1.81 +    using add_imp_eq eq mult_zero_left by (simp add: cnd)
    1.82 +  then show False using add_mult_solve [of 0 d] nz cnd by simp
    1.83  qed
    1.84  
    1.85  lemma add_0_iff:
    1.86    "x = x + a \<longleftrightarrow> a = 0"
    1.87 -proof-
    1.88 -  have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto
    1.89 -  thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute)
    1.90 -qed
    1.91 +  using add_imp_eq [of x a 0] by auto
    1.92  
    1.93  declare
    1.94    normalizing_comm_semiring_1_axioms [normalizer del]
    1.95 @@ -169,8 +160,8 @@
    1.96  lemmas
    1.97    normalizing_comm_semiring_1_cancel_norm_axioms =
    1.98    comm_semiring_1_cancel_norm_axioms [normalizer
    1.99 -    semiring ops: semiring_ops
   1.100 -    semiring rules: semiring_rules
   1.101 +    semiring ops: normalizing_semiring_ops
   1.102 +    semiring rules: normalizing_semiring_rules
   1.103      idom rules: noteq_reduce add_scale_eq_noteq]
   1.104  
   1.105  declaration
   1.106 @@ -184,10 +175,10 @@
   1.107  declare normalizing_comm_ring_1_axioms [normalizer del]
   1.108  
   1.109  lemmas normalizing_idom_axioms = idom_axioms [normalizer
   1.110 -  semiring ops: semiring_ops
   1.111 -  semiring rules: semiring_rules
   1.112 -  ring ops: ring_ops
   1.113 -  ring rules: ring_rules
   1.114 +  semiring ops: normalizing_semiring_ops
   1.115 +  semiring rules: normalizing_semiring_rules
   1.116 +  ring ops: normalizing_ring_ops
   1.117 +  ring rules: normalizing_ring_rules
   1.118    idom rules: noteq_reduce add_scale_eq_noteq
   1.119    ideal rules: right_minus_eq add_0_iff]
   1.120  
   1.121 @@ -199,19 +190,19 @@
   1.122  context field
   1.123  begin
   1.124  
   1.125 -lemma field_ops:
   1.126 +lemma normalizing_field_ops:
   1.127    shows "TERM (x / y)" and "TERM (inverse x)" .
   1.128  
   1.129 -lemmas field_rules = divide_inverse inverse_eq_divide
   1.130 +lemmas normalizing_field_rules = divide_inverse inverse_eq_divide
   1.131  
   1.132  lemmas normalizing_field_axioms =
   1.133    field_axioms [normalizer
   1.134 -    semiring ops: semiring_ops
   1.135 -    semiring rules: semiring_rules
   1.136 -    ring ops: ring_ops
   1.137 -    ring rules: ring_rules
   1.138 -    field ops: field_ops
   1.139 -    field rules: field_rules
   1.140 +    semiring ops: normalizing_semiring_ops
   1.141 +    semiring rules: normalizing_semiring_rules
   1.142 +    ring ops: normalizing_ring_ops
   1.143 +    ring rules: normalizing_ring_rules
   1.144 +    field ops: normalizing_field_ops
   1.145 +    field rules: normalizing_field_rules
   1.146      idom rules: noteq_reduce add_scale_eq_noteq
   1.147      ideal rules: right_minus_eq add_0_iff]
   1.148  
   1.149 @@ -221,12 +212,12 @@
   1.150  end
   1.151  
   1.152  hide_fact (open) normalizing_comm_semiring_1_axioms
   1.153 -  normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules
   1.154 +  normalizing_comm_semiring_1_cancel_norm_axioms normalizing_semiring_ops normalizing_semiring_rules
   1.155  
   1.156  hide_fact (open) normalizing_comm_ring_1_axioms
   1.157 -  normalizing_idom_axioms ring_ops ring_rules
   1.158 +  normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules
   1.159  
   1.160 -hide_fact (open) normalizing_field_axioms field_ops field_rules
   1.161 +hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
   1.162  
   1.163  hide_fact (open) add_scale_eq_noteq noteq_reduce
   1.164