# HG changeset patch
# User nipkow
# Date 1021642859 -7200
# Node ID 2af7b94892ce411f0bb783ef841f0becfa271d44
# Parent  8e86582a90d115fbeeba70baddefa13935d37465
Turned into Isar theories.

diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 17 11:36:32 2002 +0200
+++ b/src/HOL/IsaMakefile	Fri May 17 15:40:59 2002 +0200
@@ -569,12 +569,12 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
   ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
-  ex/Hilbert_Classical.thy ex/InSort.ML ex/InSort.thy ex/IntRing.ML \
+  ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
   ex/IntRing.thy ex/Intuitionistic.thy \
   ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy \
   ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
   ex/NatSum.thy ex/PER.thy ex/Primrec.thy ex/Puzzle.thy \
-  ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
+  ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
   ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
   ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
   ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Fri May 17 11:36:32 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/ex/insort.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-Correctness proof of insertion sort.
-*)
-
-Goal "!y. multiset(ins le x xs) y = multiset (x#xs) y";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "multiset_ins";
-Addsimps [multiset_ins];
-
-Goal "!x. multiset(insort le xs) x = multiset xs x";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "insort_permutes";
-
-Goal "set(ins le x xs) = insert x (set xs)";
-by (asm_simp_tac (simpset() addsimps [set_via_multiset]) 1);
-by (Fast_tac 1);
-qed "set_ins";
-Addsimps [set_ins];
-
-Goal "total(le) --> transf(le) --> sorted le (ins le x xs) = sorted le xs";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
-by (Blast_tac 1);
-qed_spec_mp "sorted_ins";
-Addsimps [sorted_ins];
-
-Goal "[| total(le); transf(le) |] ==>  sorted le (insort le xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "sorted_insort";
diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Fri May 17 11:36:32 2002 +0200
+++ b/src/HOL/ex/InSort.thy	Fri May 17 15:40:59 2002 +0200
@@ -6,17 +6,43 @@
 Insertion sort
 *)
 
-InSort  =  Sorting +
+theory InSort  =  Sorting:
 
 consts
-  ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
-  insort :: [['a,'a]=>bool, 'a list] => 'a list
+  ins :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
 primrec
   "ins le x [] = [x]"
   "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"
+
 primrec
   "insort le [] = []"
   "insort le (x#xs) = ins le x (insort le xs)"
+
+
+lemma multiset_ins[simp]:
+ "\<And>y. multiset(ins le x xs) y = multiset (x#xs) y"
+by (induct "xs") auto
+
+lemma insort_permutes[simp]:
+ "\<And>x. multiset(insort le xs) x = multiset xs x";
+by (induct "xs") auto
+
+lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)"
+by (simp add: set_via_multiset) fast
+
+lemma sorted_ins[simp]:
+ "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
+apply (induct xs)
+apply simp_all
+apply (unfold Sorting.total_def Sorting.transf_def)
+apply blast
+done
+
+lemma sorted_insort:
+ "[| total(le); transf(le) |] ==>  sorted le (insort le xs)"
+by (induct xs) auto
+
 end
 
diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri May 17 11:36:32 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(*  Title:      HOL/ex/Qsort.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow (tidied by lcp)
-    Copyright   1994 TU Muenchen
-
-The verification of Quicksort
-*)
-
-(*** Version one: higher-order ***)
-
-Goal "multiset (qsort(le,xs)) x = multiset xs x";
-by (induct_thm_tac qsort.induct "le xs" 1);
-by Auto_tac;
-qed "qsort_permutes";
-Addsimps [qsort_permutes];
-
-(*Also provable by induction*)
-Goal "set (qsort(le,xs)) = set xs";
-by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
-qed "set_qsort";
-Addsimps [set_qsort];
-
-Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
-by (induct_thm_tac qsort.induct "le xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
-by (Blast_tac 1);
-qed_spec_mp "sorted_qsort";
-
-
-(*** Version two: type classes ***)
-
-Goal "multiset (quickSort xs) z = multiset xs z";
-by (res_inst_tac [("x","xs")] quickSort.induct 1);
-by Auto_tac;
-qed "quickSort_permutes";
-Addsimps [quickSort_permutes];
-
-(*Also provable by induction*)
-Goal "set (quickSort xs) = set xs";
-by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
-qed "set_quickSort";
-Addsimps [set_quickSort];
-
-Goal "sorted (op <=) (quickSort xs)";
-by (res_inst_tac [("x","xs")] quickSort.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
-qed_spec_mp "sorted_quickSort";
diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Fri May 17 11:36:32 2002 +0200
+++ b/src/HOL/ex/Qsort.thy	Fri May 17 15:40:59 2002 +0200
@@ -6,28 +6,58 @@
 Quicksort
 *)
 
-Qsort = Sorting +
+theory Qsort = Sorting:
 
 (*Version one: higher-order*)
-consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
+consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"
 
 recdef qsort "measure (size o snd)"
-    simpset "simpset() addsimps [length_filter RS le_less_trans]"
-    
-    "qsort(le, [])   = []"
-    
-    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
-                       @ (x # qsort(le, [y:xs . le x y]))"
+"qsort(le, [])   = []"
+"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
+                   qsort(le, [y:xs . le x y])"
+(hints recdef_simp: length_filter[THEN le_less_trans])
+
+lemma qsort_permutes[simp]:
+ "multiset (qsort(le,xs)) x = multiset xs x"
+by (induct le xs rule: qsort.induct, auto)
+
+
+(*Also provable by induction*)
+lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
+by(simp add: set_via_multiset)
+
+lemma sorted_qsort:
+ "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
+apply (induct le xs rule: qsort.induct)
+ apply simp
+apply simp
+apply(unfold Sorting.total_def Sorting.transf_def)
+apply blast
+done
 
 
 (*Version two: type classes*)
+
 consts quickSort :: "('a::linorder) list => 'a list"
 
 recdef quickSort "measure size"
-    simpset "simpset() addsimps [length_filter RS le_less_trans]"
-    
-    "quickSort []   = []"
-    
-    "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])"
+"quickSort []   = []"
+"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
+(hints recdef_simp: length_filter[THEN le_less_trans])
+
+lemma quickSort_permutes[simp]:
+ "multiset (quickSort xs) z = multiset xs z"
+by (induct xs rule: quickSort.induct) auto
+
+(*Also provable by induction*)
+lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
+by(simp add: set_via_multiset)
+
+lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
+apply (induct xs rule: quickSort.induct)
+ apply simp
+apply simp
+apply(blast intro: linorder_linear[THEN disjE] order_trans)
+done
 
 end
diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Fri May 17 11:36:32 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      HOL/ex/sorting.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
-
-Some general lemmas
-*)
-
-Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "multiset_append";
-
-Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "multiset_compl_add";
-
-Addsimps [multiset_append, multiset_compl_add];
-
-Goal "set xs = {x. multiset xs x ~= 0}";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_via_multiset";
-
-(* Equivalence of two definitions of `sorted' *)
-
-Goal "transf(le) ==> sorted1 le xs = sorted le xs";
-by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split])));
-by (rewtac transf_def);
-by (Blast_tac 1);
-qed "sorted1_is_sorted";
-
-Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
-\                         (ALL x:set xs. ALL y:set ys. le x y))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "sorted_append";
-Addsimps [sorted_append];
-
diff -r 8e86582a90d1 -r 2af7b94892ce src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Fri May 17 11:36:32 2002 +0200
+++ b/src/HOL/ex/Sorting.thy	Fri May 17 15:40:59 2002 +0200
@@ -6,11 +6,12 @@
 Specification of sorting
 *)
 
-Sorting = Main +
+theory Sorting = Main:
+
 consts
-  sorted1:: [['a,'a] => bool, 'a list] => bool
-  sorted :: [['a,'a] => bool, 'a list] => bool
-  multiset   :: 'a list => ('a => nat)
+  sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+  sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+  multiset   :: "'a list => ('a => nat)"
 
 primrec
   "sorted1 le [] = True"
@@ -26,10 +27,39 @@
   "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
 
 constdefs
-  total  :: (['a,'a] => bool) => bool
+  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    "total r == (ALL x y. r x y | r y x)"
   
-  transf :: (['a,'a] => bool) => bool
+  transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    "transf f == (ALL x y z. f x y & f y z --> f x z)"
 
+(* Some general lemmas *)
+
+lemma multiset_append[simp]:
+ "multiset (xs@ys) x = multiset xs x + multiset ys x"
+by (induct xs, auto)
+
+lemma multiset_compl_add[simp]:
+ "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
+by (induct xs, auto)
+
+lemma set_via_multiset: "set xs = {x. multiset xs x ~= 0}";
+by (induct xs, auto)
+
+(* Equivalence of two definitions of `sorted' *)
+
+lemma sorted1_is_sorted:
+ "transf(le) ==> sorted1 le xs = sorted le xs";
+apply(induct xs)
+ apply simp
+apply(simp split: list.split)
+apply(unfold transf_def);
+apply(blast)
+done
+
+lemma sorted_append[simp]:
+ "sorted le (xs@ys) = (sorted le xs \<and> sorted le ys \<and>
+                       (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
+by (induct xs, auto)
+
 end