# HG changeset patch
# User nipkow
# Date 1094839454 -7200
# Node ID 19e735596e511042cb9c231bcf400bd7baf2badc
# Parent  c7d69df5848243ed54e122ea74a7bc0868920f1d
Added antisymmetry simproc

diff -r c7d69df58482 -r 19e735596e51 src/HOL/HOL.thy
--- 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
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Hoare/Examples.thy
--- 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
diff -r c7d69df58482 -r 19e735596e51 src/HOL/HoareParallel/Gar_Coll.thy
--- 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
diff -r c7d69df58482 -r 19e735596e51 src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- 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
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Hyperreal/Integration.thy
--- 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:
diff -r c7d69df58482 -r 19e735596e51 src/HOL/IsaMakefile
--- 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
 
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Library/While_Combinator.thy
--- 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
 
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Matrix/MatrixGeneral.thy
--- 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
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Matrix/SparseMatrix.thy
--- 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)))"
diff -r c7d69df58482 -r 19e735596e51 src/HOL/NumberTheory/Chinese.thy
--- 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
 
diff -r c7d69df58482 -r 19e735596e51 src/HOL/NumberTheory/EulerFermat.thy
--- 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)
diff -r c7d69df58482 -r 19e735596e51 src/HOL/NumberTheory/WilsonRuss.thy
--- 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]:
diff -r c7d69df58482 -r 19e735596e51 src/HOL/OrderedGroup.thy
--- 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}))"
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Ring_and_Field.thy
--- 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
diff -r c7d69df58482 -r 19e735596e51 src/HOL/Subst/Unify.ML
--- 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]))));
diff -r c7d69df58482 -r 19e735596e51 src/HOL/arith_data.ML
--- 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),