# HG changeset patch
# User nipkow
# Date 853491868 -3600
# Node ID 282e9a9eae9d8965a4686cd69c1f196e20767c82
# Parent  e3d0ac75c7232212b42079ae621f9412edd79d9a
Got rid of Alls in favour of !x:set_of_list

diff -r e3d0ac75c723 -r 282e9a9eae9d src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Thu Jan 16 16:53:15 1997 +0100
+++ b/src/HOL/ex/InSort.ML	Fri Jan 17 10:04:28 1997 +0100
@@ -6,6 +6,8 @@
 Correctness proof of insertion sort.
 *)
 
+Addsimps [Ball_insert];
+
 goalw InSort.thy [Sorting.total_def]
   "!!f. [| total(f); ~f x y |] ==> f y x";
 by (Fast_tac 1);
@@ -16,29 +18,24 @@
 by (Fast_tac 1);
 qed "transfD";
 
-goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))";
+goal InSort.thy "set_of_list(ins f x xs) = insert x (set_of_list xs)";
 by (list.induct_tac "xs" 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (Fast_tac 1);
-Addsimps [result()];
-
-goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs";
-by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-qed "list_all_imp";
+qed "set_of_list_ins";
+Addsimps [set_of_list_ins];
 
 val prems = goal InSort.thy
   "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (cut_facts_tac prems 1);
-by (cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
 by (fast_tac (!claset addDs [totalD,transfD]) 1);
-Addsimps [result()];
+qed "sorted_ins";
+Addsimps [sorted_ins];
 
 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "sorted_insort";
-
diff -r e3d0ac75c723 -r 282e9a9eae9d src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Thu Jan 16 16:53:15 1997 +0100
+++ b/src/HOL/ex/Qsort.ML	Fri Jan 17 10:04:28 1997 +0100
@@ -6,92 +6,60 @@
 Two verifications of Quicksort
 *)
 
+
+Addsimps [Ball_insert,Ball_Un];
+
+(* Towards a proof of qsort_ind
+
+A short proof of Konrad's wf_minimal in WF1.ML:
+
+val [p1] = goalw WF.thy [wf_def]
+"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
+by (rtac allI 1);
+by(cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
+by (fast_tac HOL_cs 1);
+val wf_minimal = result();
+
+*)
+
+
 Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
 
 goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-result();
+qed "qsort_permutes";
 
-
-goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))";
+goal Sorting.thy "set_of_list xs = {x.mset xs x ~= 0}";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-Addsimps [result()];
-
-goal Qsort.thy
- "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
-by (list.induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-val alls_lemma=result();
-Addsimps [alls_lemma];
+by (Fast_tac 1);
+qed "set_of_list_via_mset";
 
-goal HOL.thy "((P --> Q) & (~P --> Q)) = Q";
-by (Fast_tac 1);
-val lemma = result();
+goal Qsort.thy "set_of_list(qsort le xs) = set_of_list xs";
+by(simp_tac (!simpset addsimps [set_of_list_via_mset,qsort_permutes]) 1);
+qed "set_of_list_qsort";
+Addsimps [set_of_list_qsort];
 
-goal Qsort.thy "(Alls x:qsort le xs.P(x))  =  (Alls x:xs.P(x))";
-by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1);
-by (asm_simp_tac (!simpset addsimps [lemma]) 1);
-Addsimps [result()];
+goal List.thy
+  "(!x:set_of_list[x:xs.P(x)].Q(x)) = (!x:set_of_list xs. P(x)-->Q(x))";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed"Ball_set_of_list_filter";
+Addsimps [Ball_set_of_list_filter];
 
 goal Qsort.thy
  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
-\                     (Alls x:xs. Alls y:ys. le x y))";
+\                     (!x:set_of_list xs. !y:set_of_list ys. le x y))";
 by (list.induct_tac "xs" 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (!simpset delsimps [alls_lemma]) 1);
-Addsimps [result()];
-
-
-
+by (ALLGOALS Asm_simp_tac);
+qed "sorted_append";
+Addsimps [sorted_append];
 
 goal Qsort.thy 
  "!!le. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps []) 1);
-by (asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
+by (ALLGOALS Asm_simp_tac);
 by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by (Fast_tac 1);
-result();
-
-(* A verification based on predicate calculus rather than combinators *)
-
-val sorted_Cons =
-  rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons;
-
-Addsimps [sorted_Cons];
-
-
-goal Qsort.thy "x mem qsort le xs = x mem xs";
-by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (Fast_tac 1);
-Addsimps [result()];
-
-goal Qsort.thy
- "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
-\                     (!x. x mem xs --> (!y. y mem ys --> le x y)))";
-by (list.induct_tac "xs" 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])
-                          delsimps [list_all_conj]
-                          addsimps [list_all_mem_conv]) 1);
-by (Fast_tac 1);
-Addsimps [result()];
-
-goal Qsort.thy
-  "!!xs. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
-by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by (Simp_tac 1);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_if])
-                          delsimps [list_all_conj]
-                          addsimps [list_all_mem_conv]) 1);
-by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by (Fast_tac 1);
-result();
-
-
+qed "sorted_qsort";
diff -r e3d0ac75c723 -r 282e9a9eae9d src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Thu Jan 16 16:53:15 1997 +0100
+++ b/src/HOL/ex/Sorting.thy	Fri Jan 17 10:04:28 1997 +0100
@@ -21,7 +21,7 @@
 sorted1_Cons "sorted1 f (Cons x (y#zs)) = (f x y & sorted1 f (y#zs))"
 
 sorted_Nil "sorted le []"
-sorted_Cons "sorted le (x#xs) = ((Alls y:xs. le x y) & sorted le xs)"
+sorted_Cons "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
 
 mset_Nil "mset [] y = 0"
 mset_Cons "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"