# HG changeset patch
# User nipkow
# Date 853503396 -3600
# Node ID 2af078382853c4e4188a7fe177530affb077553d
# Parent  4d68fbe6378b5c451788ab31951305ac5f0d41b0
Modified some defs and shortened proofs.

diff -r 4d68fbe6378b -r 2af078382853 src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Fri Jan 17 12:49:31 1997 +0100
+++ b/src/HOL/ex/InSort.ML	Fri Jan 17 13:16:36 1997 +0100
@@ -8,30 +8,31 @@
 
 Addsimps [Ball_insert];
 
-goalw InSort.thy [Sorting.total_def]
-  "!!f. [| total(f); ~f x y |] ==> f y x";
-by (Fast_tac 1);
-qed "totalD";
-
-goalw InSort.thy [Sorting.transf_def]
-  "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x";
-by (Fast_tac 1);
-qed "transfD";
-
-goal InSort.thy "set_of_list(ins f x xs) = insert x (set_of_list xs)";
+goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
 by (list.induct_tac "xs" 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed "mset_ins";
+Addsimps [mset_ins];
+
+goal thy "!x. mset(insort f xs) x = mset xs x";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "insort_permutes";
+
+goal thy "set_of_list(ins f x xs) = insert x (set_of_list xs)";
+by (asm_simp_tac (!simpset addsimps [set_of_list_via_mset]
+                           setloop (split_tac [expand_if])) 1);
 by (Fast_tac 1);
 qed "set_of_list_ins";
 Addsimps [set_of_list_ins];
 
-val prems = goal InSort.thy
+val prems = goalw InSort.thy [total_def,transf_def]
   "[| 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 (fast_tac (!claset addDs [totalD,transfD]) 1);
+by (Fast_tac 1);
 qed "sorted_ins";
 Addsimps [sorted_ins];
 
diff -r 4d68fbe6378b -r 2af078382853 src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Jan 17 12:49:31 1997 +0100
+++ b/src/HOL/ex/Qsort.ML	Fri Jan 17 13:16:36 1997 +0100
@@ -30,12 +30,6 @@
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "qsort_permutes";
 
-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]))));
-by (Fast_tac 1);
-qed "set_of_list_via_mset";
-
 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";
diff -r 4d68fbe6378b -r 2af078382853 src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Fri Jan 17 12:49:31 1997 +0100
+++ b/src/HOL/ex/Sorting.ML	Fri Jan 17 13:16:36 1997 +0100
@@ -6,14 +6,10 @@
 Some general lemmas
 *)
 
-Addsimps [Sorting.mset_Nil,Sorting.mset_Cons,
-          Sorting.sorted_Nil,Sorting.sorted_Cons,
-          Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
-
 goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-qed "mset_app_distr";
+qed "mset_append";
 
 goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \
 \                     mset xs x";
@@ -21,4 +17,20 @@
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mset_compl_add";
 
-Addsimps [mset_app_distr, mset_compl_add];
+Addsimps [mset_append, mset_compl_add];
+
+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]))));
+by (Fast_tac 1);
+qed "set_of_list_via_mset";
+
+(* Equivalence of two definitions of `sorted' *)
+
+val prems = goalw Sorting.thy [transf_def]
+  "transf(le) ==> sorted1 le xs = sorted le xs";
+by (list.induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_list_case]))));
+by (cut_facts_tac prems 1);
+by (Fast_tac 1);
+qed "sorted1_is_sorted";
diff -r 4d68fbe6378b -r 2af078382853 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Fri Jan 17 12:49:31 1997 +0100
+++ b/src/HOL/ex/Sorting.thy	Fri Jan 17 13:16:36 1997 +0100
@@ -14,18 +14,20 @@
   total  :: (['a,'a] => bool) => bool
   transf :: (['a,'a] => bool) => bool
 
-rules
-
-sorted1_Nil  "sorted1 f []"
-sorted1_One  "sorted1 f [x]"
-sorted1_Cons "sorted1 f (Cons x (y#zs)) = (f x y & sorted1 f (y#zs))"
+primrec sorted1 list
+  "sorted1 le [] = True"
+  "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
+                        sorted1 le xs)"
 
-sorted_Nil "sorted le []"
-sorted_Cons "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
+primrec sorted list
+  "sorted le [] = True"
+  "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)"
+primrec mset list
+  "mset [] y = 0"
+  "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
 
+defs
 total_def  "total r == (!x y. r x y | r y x)"
 transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
 end