tuned proofs;
authorwenzelm
Tue Sep 19 23:15:28 2006 +0200 (2006-09-19)
changeset 20622e1a573146be5
parent 20621 29d57880ba00
child 20623 6ae83d153dd4
tuned proofs;
src/HOL/Library/Commutative_Ring.thy
     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.30  text {* Addition *}
    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.46      (simp_all add: mkPX_ci mkPinj_ci ring_eq_simps add_ci power_add)
    1.47  
    1.48  text {* Substraction *}
    1.49 @@ -254,65 +254,72 @@
    1.50    by (simp add: add_ci neg_ci sub_def)
    1.51  
    1.52  text {* Square *}
    1.53 -lemma sqr_ci:"\<And>ls. Ipol ls (sqr p) = Ipol ls p * Ipol ls p"
    1.54 -  by (induct p) (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_eq_simps power_add)
    1.55 +lemma sqr_ci: "Ipol ls (sqr p) = Ipol ls p * Ipol ls p"
    1.56 +  by (induct p arbitrary: ls)
    1.57 +    (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci ring_eq_simps power_add)
    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.140    by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
   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