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)