author wenzelm Tue Sep 19 23:15:28 2006 +0200 (2006-09-19) changeset 20622 e1a573146be5 parent 20621 29d57880ba00 child 20623 6ae83d153dd4
tuned proofs;
```     1.1 --- a/src/HOL/Library/Commutative_Ring.thy	Tue Sep 19 23:15:26 2006 +0200
1.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Tue Sep 19 23:15:28 2006 +0200
1.3 @@ -19,7 +19,7 @@
1.4    | PX "'a pol" nat "'a pol"
1.5
1.6  datatype 'a polex =
1.7 -  Pol "'a pol"
1.8 +    Pol "'a pol"
1.9    | Add "'a polex" "'a polex"
1.10    | Sub "'a polex" "'a polex"
1.11    | Mul "'a polex" "'a polex"
1.12 @@ -139,7 +139,7 @@
1.13      mkPX (mul (mul (Pc (1 + 1), A), mkPinj 1 B)) x (Pc 0))"
1.14
1.15  text {* Fast Exponentation *}
1.16 -lemma pow_wf:"odd n \<Longrightarrow> (n::nat) div 2 < n" by (cases n) auto
1.17 +lemma pow_wf: "odd n \<Longrightarrow> (n::nat) div 2 < n" by (cases n) auto
1.18  recdef pow "measure (\<lambda>(x, y). y)"
1.19    "pow (p, 0) = Pc 1"
1.20    "pow (p, n) = (if even n then (pow (sqr p, n div 2)) else mul (p, pow (sqr p, n div 2)))"
1.21 @@ -191,12 +191,12 @@
1.22  text {* Correctness theorems for the implemented operations *}
1.23
1.24  text {* Negation *}
1.25 -lemma neg_ci: "\<And>l. Ipol l (neg P) = -(Ipol l P)"
1.26 -  by (induct P) auto
1.27 +lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
1.28 +  by (induct P arbitrary: l) auto
1.29
1.31 -lemma add_ci: "\<And>l. Ipol l (add (P, Q)) = Ipol l P + Ipol l Q"
1.32 -proof (induct P Q rule: add.induct)
1.33 +lemma add_ci: "Ipol l (add (P, Q)) = Ipol l P + Ipol l Q"
1.34 +proof (induct P Q arbitrary: l rule: add.induct)
1.35    case (6 x P y Q)
1.36    show ?case
1.37    proof (rule linorder_cases)
1.38 @@ -245,8 +245,8 @@
1.39  qed (auto simp add: ring_eq_simps)
1.40
1.41  text {* Multiplication *}
1.42 -lemma mul_ci: "\<And>l. Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"
1.43 -  by (induct P Q rule: mul.induct)
1.44 +lemma mul_ci: "Ipol l (mul (P, Q)) = Ipol l P * Ipol l Q"
1.45 +  by (induct P Q arbitrary: l rule: mul.induct)
1.47
1.48  text {* Substraction *}
1.49 @@ -254,65 +254,72 @@
1.51
1.52  text {* Square *}
1.53 -lemma sqr_ci:"\<And>ls. Ipol ls (sqr p) = Ipol ls p * Ipol ls p"
1.55 +lemma sqr_ci: "Ipol ls (sqr p) = Ipol ls p * Ipol ls p"
1.56 +  by (induct p arbitrary: ls)
1.58
1.59
1.60  text {* Power *}
1.61 -lemma even_pow:"even n \<Longrightarrow> pow (p, n) = pow (sqr p, n div 2)" by (induct n) simp_all
1.62 +lemma even_pow:"even n \<Longrightarrow> pow (p, n) = pow (sqr p, n div 2)"
1.63 +  by (induct n) simp_all
1.64
1.65 -lemma pow_ci: "\<And>p. Ipol ls (pow (p, n)) = (Ipol ls p) ^ n"
1.66 -proof (induct n rule: nat_less_induct)
1.67 +lemma pow_ci: "Ipol ls (pow (p, n)) = Ipol ls p ^ n"
1.68 +proof (induct n arbitrary: p rule: nat_less_induct)
1.69    case (1 k)
1.70 -  have two:"2 = Suc (Suc 0)" by simp
1.71 +  have two: "2 = Suc (Suc 0)" by simp
1.72    show ?case
1.73    proof (cases k)
1.74 +    case 0
1.75 +    then show ?thesis by simp
1.76 +  next
1.77      case (Suc l)
1.78      show ?thesis
1.79      proof cases
1.80 -      assume EL: "even l"
1.81 -      have "Suc l div 2 = l div 2"
1.82 -        by (simp add: nat_number even_nat_plus_one_div_two [OF EL])
1.83 +      assume "even l"
1.84 +      then have "Suc l div 2 = l div 2"
1.85 +        by (simp add: nat_number even_nat_plus_one_div_two)
1.86        moreover
1.87        from Suc have "l < k" by simp
1.88 -      with 1 have "\<forall>p. Ipol ls (pow (p, l)) = Ipol ls p ^ l" by simp
1.89 +      with 1 have "\<And>p. Ipol ls (pow (p, l)) = Ipol ls p ^ l" by simp
1.90        moreover
1.91 -      note Suc EL even_nat_plus_one_div_two [OF EL]
1.92 +      note Suc `even l` even_nat_plus_one_div_two
1.93        ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow)
1.94      next
1.95 -      assume OL: "odd l"
1.96 -      with prems have "\<lbrakk>\<forall>m<Suc l. \<forall>p. Ipol ls (pow (p, m)) = Ipol ls p ^ m; k = Suc l; odd l\<rbrakk> \<Longrightarrow> \<forall>p. Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l"
1.97 -      proof(cases l)
1.98 -        case (Suc w)
1.99 -        from prems have EW: "even w" by simp
1.100 -        from two have two_times:"(2 * (w div 2))= w"
1.101 -          by (simp only: even_nat_div_two_times_two[OF EW])
1.102 -        have A: "\<And>p. (Ipol ls p * Ipol ls p) = (Ipol ls p) ^ (Suc (Suc 0))"
1.103 -          by (simp add: power_Suc)
1.104 -        from A two [symmetric] have "ALL p.(Ipol ls p * Ipol ls p) = (Ipol ls p) ^ 2"
1.105 -          by simp
1.106 -        with prems show ?thesis
1.107 -          by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
1.108 -      qed simp
1.109 -      with prems show ?thesis by simp
1.110 +      assume "odd l"
1.111 +      {
1.112 +        fix p
1.113 +        have "Ipol ls (sqr p) ^ (Suc l div 2) = Ipol ls p ^ Suc l"
1.114 +        proof (cases l)
1.115 +          case 0
1.116 +          with `odd l` show ?thesis by simp
1.117 +        next
1.118 +          case (Suc w)
1.119 +          with `odd l` have "even w" by simp
1.120 +          from two have two_times: "2 * (w div 2) = w"
1.121 +            by (simp only: even_nat_div_two_times_two [OF `even w`])
1.122 +          have "Ipol ls p * Ipol ls p = Ipol ls p ^ Suc (Suc 0)"
1.123 +            by (simp add: power_Suc)
1.124 +          from this and two [symmetric] have "Ipol ls p * Ipol ls p = Ipol ls p ^ 2"
1.125 +            by simp
1.126 +          with Suc show ?thesis
1.127 +            by (auto simp add: power_mult[symmetric, of _ 2 _] two_times mul_ci sqr_ci)
1.128 +        qed
1.129 +      } with 1 Suc `odd l` show ?thesis by simp
1.130      qed
1.131 -  next
1.132 -    case 0
1.133 -    then show ?thesis by simp
1.134    qed
1.135  qed
1.136
1.137  text {* Normalization preserves semantics  *}
1.138 -lemma norm_ci:"Ipolex l Pe = Ipol l (norm Pe)"
1.139 +lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
1.141
1.142  text {* Reflection lemma: Key to the (incomplete) decision procedure *}
1.143  lemma norm_eq:
1.144 -  assumes eq: "norm P1  = norm P2"
1.145 +  assumes "norm P1 = norm P2"
1.146    shows "Ipolex l P1 = Ipolex l P2"
1.147  proof -
1.148 -  from eq have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
1.149 -  thus ?thesis by (simp only: norm_ci)
1.150 +  from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
1.151 +  then show ?thesis by (simp only: norm_ci)
1.152  qed
1.153
1.154
```