--- a/src/HOL/HOL.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/HOL.thy Fri Sep 10 20:04:14 2004 +0200
@@ -8,6 +8,7 @@
theory HOL
imports CPure
files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+ ("antisym_setup.ML")
begin
subsection {* Primitive logic *}
@@ -737,6 +738,8 @@
lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
by (blast intro: order_antisym)
+lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
+by(blast intro:order_antisym)
text {* Transitivity. *}
@@ -848,6 +851,17 @@
lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
by (simp add: linorder_neq_iff, blast)
+lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
+by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+
+lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
+by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+
+lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
+by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
+
+use "antisym_setup.ML";
+setup antisym_setup
subsubsection "Min and max on (linear) orders"
@@ -927,8 +941,6 @@
lemma max_commute: "!!x::'a::linorder. max x y = max y x"
apply(simp add:max_def)
-apply(rule conjI)
-apply(blast intro:order_antisym)
apply(simp add:linorder_not_le)
apply(blast dest: order_less_trans)
done
@@ -946,8 +958,6 @@
lemma min_commute: "!!x::'a::linorder. min x y = min y x"
apply(simp add:min_def)
-apply(rule conjI)
-apply(blast intro:order_antisym)
apply(simp add:linorder_not_le)
apply(blast dest: order_less_trans)
done
--- a/src/HOL/Hoare/Examples.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Hoare/Examples.thy Fri Sep 10 20:04:14 2004 +0200
@@ -32,9 +32,6 @@
apply vcg_simp
apply (simp add:int_distrib)
apply clarsimp
-apply(subgoal_tac "M=0")
- prefer 2 apply simp
-apply clarsimp
apply(rule conjI)
apply clarsimp
apply clarsimp
--- a/src/HOL/HoareParallel/Gar_Coll.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Fri Sep 10 20:04:14 2004 +0200
@@ -128,7 +128,6 @@
apply(simp_all add:nth_list_update)
apply (erule less_SucE)
apply simp+
- apply(drule le_imp_less_or_eq)
apply force
apply force
done
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Sep 10 20:04:14 2004 +0200
@@ -202,7 +202,6 @@
apply(simp_all add:nth_list_update)
apply (erule less_SucE)
apply simp+
- apply(drule le_imp_less_or_eq)
apply force
apply force
done
--- a/src/HOL/Hyperreal/Integration.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Fri Sep 10 20:04:14 2004 +0200
@@ -739,9 +739,8 @@
apply (rule partition [THEN iffD2])
apply (frule partition [THEN iffD1])
apply (auto intro: partition_lt_gen)
-apply (drule_tac n = n in partition_lt_gen)
-apply (assumption, arith, blast)
-apply (drule partition_lt_cancel, auto)
+ apply (drule (1) partition_lt_cancel, arith)
+apply (drule (1) partition_lt_cancel, arith)
done
lemma fine_left1:
--- a/src/HOL/IsaMakefile Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 10 20:04:14 2004 +0200
@@ -113,7 +113,8 @@
Tools/split_rule.ML Tools/typedef_package.ML \
Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
- Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
+ Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
+ blastdata.ML cladata.ML \
document/root.tex hologic.ML simpdata.ML thy_syntax.ML
@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
--- a/src/HOL/Library/While_Combinator.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Library/While_Combinator.thy Fri Sep 10 20:04:14 2004 +0200
@@ -143,6 +143,13 @@
An example of using the @{term while} combinator.
*}
+text{* Cannot use @{thm[source]set_eq_subset} because it leads to
+looping because the antisymmetry simproc turns the subset relationship
+back into equality. *}
+
+lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
+by blast
+
theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
P {0, 4, 2}"
proof -
@@ -156,7 +163,7 @@
apply simp
apply (simp add: aux set_eq_subset)
txt {* The fixpoint computation is performed purely by rewriting: *}
- apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
+ apply (simp add: while_unfold aux seteq del: subset_empty)
done
qed
--- a/src/HOL/Matrix/MatrixGeneral.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Fri Sep 10 20:04:14 2004 +0200
@@ -496,8 +496,6 @@
lemma foldseq_tail: "M <= N \<Longrightarrow> foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \<Longrightarrow> ?concl")
proof -
have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
- have suc2: "!! a b. \<lbrakk>a <= Suc b; ~ (a <= b)\<rbrakk> \<Longrightarrow> a = (Suc b)" by arith
- have eq: "!! (a::nat) b. \<lbrakk>~(a < b); a <= b\<rbrakk> \<Longrightarrow> a = b" by arith
have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
have "!! n. ! m s. m <= n \<longrightarrow> foldseq f s n = foldseq f (% k. (if k < m then (s k) else (foldseq f (% k. s(k+m)) (n-m)))) m"
apply (induct_tac n)
@@ -508,8 +506,7 @@
apply (simp)
apply (rule a)
apply (rule foldseq_significant_positions)
- apply (simp, auto)
- apply (drule eq, simp+)
+ apply (auto)
apply (drule suc, simp+)
proof -
fix na m s
@@ -540,17 +537,12 @@
and nm: "n <= m"
shows
"foldseq f s n = foldseq f s m"
-proof -
- have a: "!! a b. ~(a < b) \<Longrightarrow> a <= b \<Longrightarrow> (a::nat) = b" by simp
- show "foldseq f s n = foldseq f s m"
apply (simp add: foldseq_tail[OF nm, of f s])
apply (rule foldseq_significant_positions)
apply (auto)
- apply (drule a)
- apply (simp+)
apply (subst foldseq_zero)
by (simp add: fz sz)+
-qed
+
lemma foldseq_zerotail2:
assumes "! x. f x 0 = x"
@@ -560,7 +552,6 @@
"foldseq f s n = foldseq f s m" (is ?concl)
proof -
have "f 0 0 = 0" by (simp add: prems)
- have a:"!! (i::nat) m. ~(i < m) \<Longrightarrow> i <= m \<Longrightarrow> i = m" by arith
have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
have c: "0 <= m" by simp
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
@@ -569,11 +560,9 @@
apply (rule foldseq_significant_positions)
apply (auto)
apply (case_tac "m=n")
- apply (drule a, simp+)
+ apply (simp+)
apply (drule b[OF nm])
apply (auto)
- apply (drule a)
- apply simp+
apply (case_tac "k=0")
apply (simp add: prems)
apply (drule d)
@@ -674,7 +663,7 @@
assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
proof -
- from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
+ from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n[where n = n])
also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
qed
--- a/src/HOL/Matrix/SparseMatrix.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Fri Sep 10 20:04:14 2004 +0200
@@ -188,8 +188,6 @@
(sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
apply (rule addmult_spvec.induct[of _ y])
apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
- apply (case_tac "a=aa")
- apply (auto)
done
lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
@@ -403,8 +401,6 @@
lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)"
apply (rule add_spvec.induct[of _ a b])
apply (simp_all add: singleton_matrix_add)
- apply (case_tac "a = aa")
- apply (simp_all)
done
recdef add_spmat "measure (% (A,B). (length A)+(length B))"
@@ -421,7 +417,6 @@
lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)"
apply (rule add_spmat.induct)
apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
- apply (case_tac "a=aa", simp, simp)+
done
lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
--- a/src/HOL/NumberTheory/Chinese.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Fri Sep 10 20:04:14 2004 +0200
@@ -92,10 +92,9 @@
"k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
apply (induct l)
apply auto
- apply (rule_tac [2] zdvd_zmult2)
- apply (rule_tac [3] zdvd_zmult)
- apply (subgoal_tac "i = k")
- apply (subgoal_tac [3] "i = Suc (k + n)")
+ apply (rule_tac [1] zdvd_zmult2)
+ apply (rule_tac [2] zdvd_zmult)
+ apply (subgoal_tac "i = Suc (k + n)")
apply (simp_all (no_asm_simp))
done
--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Fri Sep 10 20:04:14 2004 +0200
@@ -102,11 +102,6 @@
lemma Bnor_mem_if [rule_format]:
"zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
apply (induct a m rule: BnorRset.induct, auto)
- apply (case_tac "a = b")
- prefer 2
- apply (simp add: order_less_le)
- apply (simp (no_asm_simp))
- prefer 2
apply (subst BnorRset.simps)
defer
apply (subst BnorRset.simps)
--- a/src/HOL/NumberTheory/WilsonRuss.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Fri Sep 10 20:04:14 2004 +0200
@@ -224,11 +224,9 @@
"p \<in> zprime -->
a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
apply (induct a p rule: wset.induct, auto)
- apply (subgoal_tac "b = a")
- apply (rule_tac [2] zle_anti_sym)
- apply (rule_tac [4] wset_subset)
- apply (simp (no_asm_simp))
- apply auto
+ apply (rule_tac wset_subset)
+ apply (simp (no_asm_simp))
+ apply auto
done
lemma wset_mem_inv_mem [rule_format]:
--- a/src/HOL/OrderedGroup.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/OrderedGroup.thy Fri Sep 10 20:04:14 2004 +0200
@@ -661,10 +661,7 @@
proof -
note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
- show ?thesis
- apply (auto simp add: join_max max_def b linorder_not_less)
- apply (drule order_antisym, auto)
- done
+ show ?thesis by (auto simp add: join_max max_def b linorder_not_less)
qed
lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
--- a/src/HOL/Ring_and_Field.thy Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy Fri Sep 10 20:04:14 2004 +0200
@@ -1434,8 +1434,9 @@
apply (auto simp add:
ring_eq_simps
iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
- iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id]
- order_antisym mult_pos_neg_le[of a b] mult_pos_neg2_le[of b a])
+ iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
+ apply(drule (1) mult_pos_neg_le[of a b], simp)
+ apply(drule (1) mult_pos_neg2_le[of b a], simp)
done
next
assume "~(0 <= a*b)"
@@ -1444,7 +1445,9 @@
apply (simp_all add: mulprts abs_prts)
apply (insert prems)
apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
- iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_le[of a b] mult_neg_le[of a b])
+ iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
+ apply(drule (1) mult_pos_le[of a b],simp)
+ apply(drule (1) mult_neg_le[of a b],simp)
done
qed
qed
--- a/src/HOL/Subst/Unify.ML Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/Subst/Unify.ML Fri Sep 10 20:04:14 2004 +0200
@@ -100,7 +100,7 @@
(simpset() addsimps [unifyRel_def, lex_prod_def,
measure_def, inv_image_def]) 1);
by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
- psubset_def, set_eq_subset]) 1);
+ psubset_def]) 1);
by (Blast_tac 1);
(** LEVEL 9 **)
(*Final case, also finite_psubset*)
@@ -112,7 +112,7 @@
by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq])));
by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
by (ALLGOALS (asm_full_simp_tac
- (simpset() addsimps [srange_iff, set_eq_subset])));
+ (simpset() addsimps [srange_iff])));
by (ALLGOALS
(fast_tac (claset() addEs [Var_intro RS disjE]
addss (simpset() addsimps [srange_iff]))));
--- a/src/HOL/arith_data.ML Fri Sep 10 14:54:54 2004 +0200
+++ b/src/HOL/arith_data.ML Fri Sep 10 20:04:14 2004 +0200
@@ -482,7 +482,7 @@
end;
(* antisymmetry:
- combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y *)
+ combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
local
val antisym = mk_meta_eq order_antisym
@@ -523,13 +523,12 @@
end
handle THM _ => []
end;
-
+*)
(* theory setup *)
val arith_setup =
- [Simplifier.change_simpset_of (op setmksimps2) antisym_eq,
- Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
+ [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
init_lin_arith_data @
[Simplifier.change_simpset_of (op addSolver)
(mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),