tuned proofs
authorChristian Urban <urbanc@in.tum.de>
Mon Apr 02 21:26:07 2012 +0100 (2012-04-02)
changeset 47304a0d97d919f01
parent 47301 ca743eafa1dd
child 47305 ce898681f700
tuned proofs
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Apr 02 18:12:53 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Apr 02 21:26:07 2012 +0100
     1.3 @@ -255,31 +255,25 @@
     1.4    minus_add_distrib[of z1 z2]
     1.5    for z1 z2 w :: int
     1.6  
     1.7 -lemma int_induct_raw:
     1.8 -  assumes a: "P (0::nat, 0)"
     1.9 -  and     b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
    1.10 -  and     c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
    1.11 -  shows      "P x"
    1.12 -proof (cases x, clarify)
    1.13 -  fix a b
    1.14 -  show "P (a, b)"
    1.15 -  proof (induct a arbitrary: b rule: nat.induct)
    1.16 -    case zero
    1.17 -    show "P (0, b)" using assms by (induct b) auto
    1.18 -  next
    1.19 -    case (Suc n)
    1.20 -    then show ?case using assms by auto
    1.21 -  qed
    1.22 -qed
    1.23 +lemma int_induct2:
    1.24 +  assumes "P 0 0"
    1.25 +  and     "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
    1.26 +  and     "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
    1.27 +  shows   "P n m"
    1.28 +using assms
    1.29 +by (induction_schema) (pat_completeness, lexicographic_order)
    1.30 +
    1.31  
    1.32  lemma int_induct:
    1.33 -  fixes x :: int
    1.34 +  fixes j :: int
    1.35    assumes a: "P 0"
    1.36 -  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
    1.37 -  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
    1.38 -  shows      "P x"
    1.39 -  using a b c unfolding minus_int_def
    1.40 -  by (lifting int_induct_raw)
    1.41 +  and     b: "\<And>i::int. P i \<Longrightarrow> P (i + 1)"
    1.42 +  and     c: "\<And>i::int. P i \<Longrightarrow> P (i - 1)"
    1.43 +  shows      "P j"
    1.44 +using a b c 
    1.45 +unfolding minus_int_def
    1.46 +by (descending) (auto intro: int_induct2)
    1.47 +  
    1.48  
    1.49  text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
    1.50  
    1.51 @@ -289,7 +283,8 @@
    1.52  quotient_definition
    1.53    "int_to_nat::int \<Rightarrow> nat"
    1.54  is
    1.55 -  "int_to_nat_raw" unfolding int_to_nat_raw_def by force
    1.56 +  "int_to_nat_raw" 
    1.57 +unfolding int_to_nat_raw_def by auto 
    1.58  
    1.59  lemma nat_le_eq_zle:
    1.60    fixes w z::"int"
     2.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Mon Apr 02 18:12:53 2012 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Mon Apr 02 21:26:07 2012 +0100
     2.3 @@ -307,20 +307,15 @@
     2.4    thus "Decrypt K X = Decrypt K X'" by simp
     2.5  qed
     2.6  
     2.7 -lemma msg_induct_aux:
     2.8 -  shows "\<lbrakk>\<And>N. P (Nonce N);
     2.9 -          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
    2.10 -          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
    2.11 -          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
    2.12 -  by (lifting freemsg.induct)
    2.13 -
    2.14  lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
    2.15    assumes N: "\<And>N. P (Nonce N)"
    2.16        and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
    2.17        and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
    2.18        and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
    2.19    shows "P msg"
    2.20 -  using N M C D by (rule msg_induct_aux)
    2.21 +  using N M C D 
    2.22 +  by (descending) (auto intro: freemsg.induct)
    2.23 +
    2.24  
    2.25  subsection{*The Abstract Discriminator*}
    2.26