tidying and structured proofs
authorpaulson
Sat Mar 17 12:36:11 2012 +0000 (2012-03-17)
changeset 469937371429c527d
parent 46985 bd955d9f464b
child 46994 67cf9a6308f3
tidying and structured proofs
src/ZF/IntDiv_ZF.thy
src/ZF/Ordinal.thy
src/ZF/WF.thy
     1.1 --- a/src/ZF/IntDiv_ZF.thy	Sat Mar 17 12:00:11 2012 +0100
     1.2 +++ b/src/ZF/IntDiv_ZF.thy	Sat Mar 17 12:36:11 2012 +0000
     1.3 @@ -359,7 +359,7 @@
     1.4   apply (erule zle_zless_trans)
     1.5   apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
     1.6   apply (erule zle_zless_trans)
     1.7 - apply (simp add: );
     1.8 + apply simp
     1.9  apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)")
    1.10   prefer 2
    1.11   apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
    1.12 @@ -430,16 +430,18 @@
    1.13    assumes prem:
    1.14          "!!a b. [| a \<in> int; b \<in> int;
    1.15                     ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)"
    1.16 -  shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)"
    1.17 -apply (rule_tac a = "<u,v>" in wf_induct)
    1.18 -apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"
    1.19 -       in wf_measure)
    1.20 -apply clarify
    1.21 -apply (rule prem)
    1.22 -apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
    1.23 -apply auto
    1.24 -apply (simp add: not_zle_iff_zless posDivAlg_termination)
    1.25 -done
    1.26 +  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
    1.27 +using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"]
    1.28 +proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
    1.29 +  case (step x)
    1.30 +  hence uv: "u \<in> int" "v \<in> int" by auto
    1.31 +  thus ?case
    1.32 +    apply (rule prem) 
    1.33 +    apply (rule impI) 
    1.34 +    apply (rule step) 
    1.35 +    apply (auto simp add: step uv not_zle_iff_zless posDivAlg_termination)
    1.36 +    done
    1.37 +qed
    1.38  
    1.39  
    1.40  lemma posDivAlg_induct [consumes 2]:
    1.41 @@ -459,26 +461,20 @@
    1.42  (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
    1.43      then this rewrite can work for all constants!!*)
    1.44  lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
    1.45 -apply (simp (no_asm) add: int_eq_iff_zle)
    1.46 -done
    1.47 +  by (simp add: int_eq_iff_zle)
    1.48  
    1.49  
    1.50  subsection{* Some convenient biconditionals for products of signs *}
    1.51  
    1.52  lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
    1.53 -apply (drule zmult_zless_mono1)
    1.54 -apply auto
    1.55 -done
    1.56 +  by (drule zmult_zless_mono1, auto)
    1.57  
    1.58  lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"
    1.59 -apply (drule zmult_zless_mono1_neg)
    1.60 -apply auto
    1.61 -done
    1.62 +  by (drule zmult_zless_mono1_neg, auto)
    1.63  
    1.64  lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0"
    1.65 -apply (drule zmult_zless_mono1_neg)
    1.66 -apply auto
    1.67 -done
    1.68 +  by (drule zmult_zless_mono1_neg, auto)
    1.69 +
    1.70  
    1.71  (** Inequality reasoning **)
    1.72  
    1.73 @@ -591,16 +587,18 @@
    1.74          "!!a b. [| a \<in> int; b \<in> int;
    1.75                     ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |]
    1.76                  ==> P(<a,b>)"
    1.77 -  shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)"
    1.78 -apply (rule_tac a = "<u,v>" in wf_induct)
    1.79 -apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"
    1.80 -       in wf_measure)
    1.81 -apply clarify
    1.82 -apply (rule prem)
    1.83 -apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
    1.84 -apply auto
    1.85 -apply (simp add: not_zle_iff_zless negDivAlg_termination)
    1.86 -done
    1.87 +  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
    1.88 +using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"]
    1.89 +proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
    1.90 +  case (step x)
    1.91 +  hence uv: "u \<in> int" "v \<in> int" by auto
    1.92 +  thus ?case
    1.93 +    apply (rule prem) 
    1.94 +    apply (rule impI) 
    1.95 +    apply (rule step) 
    1.96 +    apply (auto simp add: step uv not_zle_iff_zless negDivAlg_termination)
    1.97 +    done
    1.98 +qed
    1.99  
   1.100  lemma negDivAlg_induct [consumes 2]:
   1.101    assumes u_int: "u \<in> int"
   1.102 @@ -729,12 +727,10 @@
   1.103  (** intify cancellation **)
   1.104  
   1.105  lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
   1.106 -apply (simp (no_asm) add: zdiv_def)
   1.107 -done
   1.108 +  by (simp add: zdiv_def)
   1.109  
   1.110  lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
   1.111 -apply (simp (no_asm) add: zdiv_def)
   1.112 -done
   1.113 +  by (simp add: zdiv_def)
   1.114  
   1.115  lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
   1.116  apply (unfold zdiv_def)
   1.117 @@ -742,12 +738,10 @@
   1.118  done
   1.119  
   1.120  lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
   1.121 -apply (simp (no_asm) add: zmod_def)
   1.122 -done
   1.123 +  by (simp add: zmod_def)
   1.124  
   1.125  lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
   1.126 -apply (simp (no_asm) add: zmod_def)
   1.127 -done
   1.128 +  by (simp add: zmod_def)
   1.129  
   1.130  lemma zmod_type [iff,TC]: "z zmod w \<in> int"
   1.131  apply (unfold zmod_def)
   1.132 @@ -760,13 +754,10 @@
   1.133      certain equations **)
   1.134  
   1.135  lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
   1.136 -apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor)
   1.137 -done  (*NOT for adding to default simpset*)
   1.138 +  by (simp add: zdiv_def divAlg_def posDivAlg_zero_divisor)
   1.139  
   1.140  lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
   1.141 -apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor)
   1.142 -done  (*NOT for adding to default simpset*)
   1.143 -
   1.144 +  by (simp add: zmod_def divAlg_def posDivAlg_zero_divisor)
   1.145  
   1.146  
   1.147  (** Basic laws about division and remainder **)
   1.148 @@ -1021,24 +1012,19 @@
   1.149  subsection{* Computation of division and remainder *}
   1.150  
   1.151  lemma zdiv_zero [simp]: "#0 zdiv b = #0"
   1.152 -apply (simp (no_asm) add: zdiv_def divAlg_def)
   1.153 -done
   1.154 +  by (simp add: zdiv_def divAlg_def)
   1.155  
   1.156  lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
   1.157 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
   1.158 -done
   1.159 +  by (simp (no_asm_simp) add: zdiv_def divAlg_def)
   1.160  
   1.161  lemma zmod_zero [simp]: "#0 zmod b = #0"
   1.162 -apply (simp (no_asm) add: zmod_def divAlg_def)
   1.163 -done
   1.164 +  by (simp add: zmod_def divAlg_def)
   1.165  
   1.166  lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
   1.167 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
   1.168 -done
   1.169 +  by (simp add: zdiv_def divAlg_def)
   1.170  
   1.171  lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1"
   1.172 -apply (simp (no_asm_simp) add: zmod_def divAlg_def)
   1.173 -done
   1.174 +  by (simp add: zmod_def divAlg_def)
   1.175  
   1.176  (** a positive, b positive **)
   1.177  
   1.178 @@ -1350,20 +1336,16 @@
   1.179  done
   1.180  
   1.181  lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)"
   1.182 -apply (simp (no_asm_simp) add: zdiv_zmult1_eq)
   1.183 -done
   1.184 +  by (simp add: zdiv_zmult1_eq)
   1.185  
   1.186  lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)"
   1.187 -apply (subst zmult_commute , erule zdiv_zmult_self1)
   1.188 -done
   1.189 +  by (simp add: zmult_commute) 
   1.190  
   1.191  lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0"
   1.192 -apply (simp (no_asm) add: zmod_zmult1_eq)
   1.193 -done
   1.194 +  by (simp add: zmod_zmult1_eq)
   1.195  
   1.196  lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0"
   1.197 -apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq)
   1.198 -done
   1.199 +  by (simp add: zmult_commute zmod_zmult1_eq)
   1.200  
   1.201  
   1.202  (** proving (a$+b) zdiv c =
     2.1 --- a/src/ZF/Ordinal.thy	Sat Mar 17 12:00:11 2012 +0100
     2.2 +++ b/src/ZF/Ordinal.thy	Sat Mar 17 12:36:11 2012 +0000
     2.3 @@ -353,13 +353,18 @@
     2.4  
     2.5  subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
     2.6  
     2.7 -lemma Ord_linear [rule_format]:
     2.8 -     "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i\<in>j | i=j | j\<in>i)"
     2.9 -apply (erule trans_induct)
    2.10 -apply (rule impI [THEN allI])
    2.11 -apply (erule_tac i=j in trans_induct)
    2.12 -apply (blast dest: Ord_trans)
    2.13 -done
    2.14 +lemma Ord_linear:
    2.15 +     "Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i"
    2.16 +proof (induct i arbitrary: j rule: trans_induct)
    2.17 +  case (step i)
    2.18 +  note step_i = step
    2.19 +  show ?case using `Ord(j)`
    2.20 +    proof (induct j rule: trans_induct)
    2.21 +      case (step j)
    2.22 +      thus ?case using step_i
    2.23 +        by (blast dest: Ord_trans)
    2.24 +    qed
    2.25 +qed
    2.26  
    2.27  text{*The trichotomy law for ordinals*}
    2.28  lemma Ord_linear_lt:
     3.1 --- a/src/ZF/WF.thy	Sat Mar 17 12:00:11 2012 +0100
     3.2 +++ b/src/ZF/WF.thy	Sat Mar 17 12:36:11 2012 +0000
     3.3 @@ -57,7 +57,7 @@
     3.4  lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
     3.5  by (unfold wf_def wf_on_def, force)
     3.6  
     3.7 -lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)";
     3.8 +lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)"
     3.9  by (simp add: wf_on_def subset_Int_iff)
    3.10  
    3.11  lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
    3.12 @@ -105,7 +105,7 @@
    3.13  
    3.14  text{*Consider the least @{term z} in @{term "domain(r)"} such that
    3.15    @{term "P(z)"} does not hold...*}
    3.16 -lemma wf_induct [induct set: wf]:
    3.17 +lemma wf_induct_raw:
    3.18      "[| wf(r);
    3.19          !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
    3.20       ==> P(a)"
    3.21 @@ -114,7 +114,7 @@
    3.22  apply blast
    3.23  done
    3.24  
    3.25 -lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
    3.26 +lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]
    3.27  
    3.28  text{*The form of this rule is designed to match @{text wfI}*}
    3.29  lemma wf_induct2:
    3.30 @@ -128,7 +128,7 @@
    3.31  lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A"
    3.32  by blast
    3.33  
    3.34 -lemma wf_on_induct [consumes 2, induct set: wf_on]:
    3.35 +lemma wf_on_induct_raw [consumes 2, induct set: wf_on]:
    3.36      "[| wf[A](r);  a \<in> A;
    3.37          !!x.[| x \<in> A;  \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x)
    3.38       |]  ==>  P(a)"
    3.39 @@ -137,8 +137,8 @@
    3.40  apply (rule field_Int_square, blast)
    3.41  done
    3.42  
    3.43 -lemmas wf_on_induct_rule =
    3.44 -  wf_on_induct [rule_format, consumes 2, induct set: wf_on]
    3.45 +lemmas wf_on_induct =
    3.46 +  wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on]
    3.47  
    3.48  
    3.49  text{*If @{term r} allows well-founded induction
    3.50 @@ -297,6 +297,7 @@
    3.51   apply (rule lam_type [THEN restrict_type2])
    3.52    apply blast
    3.53   apply (blast dest: transD)
    3.54 +apply atomize
    3.55  apply (frule spec [THEN mp], assumption)
    3.56  apply (subgoal_tac "<xa,a1> \<in> r")
    3.57   apply (drule_tac x1 = xa in spec [THEN mp], assumption)