# HG changeset patch
# User nipkow
# Date 761994335 -3600
# Node ID a73f8a7784bd02d3d9136a821dee70f334b93d72
# Parent  3d5b2b874e1422a5c3b19fae30a18893b308b130
some more sorting algorithms

diff -r 3d5b2b874e14 -r a73f8a7784bd ex/InSort.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/InSort.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,46 @@
+(*  Title: 	HOL/ex/insort.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Correctness proof of insertion sort.
+*)
+
+val insort_ss = sorting_ss addsimps
+ [InSort.ins_Nil,InSort.ins_Cons,InSort.insort_Nil,InSort.insort_Cons];
+
+goalw InSort.thy [Sorting.total_def]
+  "!!f. [| total(f); ~f(x,y) |] ==> f(y,x)";
+by(fast_tac HOL_cs 1);
+val totalD = result();
+
+goalw InSort.thy [Sorting.transf_def]
+  "!!f. [| transf(f); f(b,a) |] ==> !x. f(a,x) --> f(b,x)";
+by(fast_tac HOL_cs 1);
+val transfD = result();
+
+goal InSort.thy "list_all(p,ins(f,x,xs)) = (list_all(p,xs) & p(x))";
+by(list_ind_tac "xs" 1);
+by(asm_simp_tac insort_ss 1);
+by(asm_simp_tac (insort_ss setloop (split_tac [expand_if])) 1);
+by(fast_tac HOL_cs 1);
+val insort_ss = insort_ss addsimps [result()];
+
+goal InSort.thy "(!x. p(x) --> q(x)) --> list_all(p,xs) --> list_all(q,xs)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
+val list_all_imp = result();
+
+val prems = goal InSort.thy
+  "[| total(f); transf(f) |] ==>  sorted(f,ins(f,x,xs)) = sorted(f,xs)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
+by(cut_facts_tac prems 1);
+by(cut_inst_tac [("p","f(xa)"),("q","f(x)")] list_all_imp 1);
+by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
+val insort_ss = insort_ss addsimps [result()];
+
+goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted(f,insort(f,xs))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac insort_ss));
+result();
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/InSort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/InSort.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,22 @@
+(*  Title: 	HOL/ex/insort.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Insertion sort
+*)
+
+InSort  =  Sorting +
+
+consts
+  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
+  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
+
+rules
+  ins_Nil  "ins(f,x,[]) = [x]"
+  ins_Cons "ins(f,x,Cons(y,ys)) =   \
+\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+
+  insort_Nil  "insort(f,[]) = []"
+  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+end
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/Qsort.ML
--- a/ex/Qsort.ML	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/Qsort.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -6,22 +6,8 @@
 Two verifications of Quicksort
 *)
 
-val ss = list_ss addsimps
- [Qsort.mset_Nil,Qsort.mset_Cons,
-  Qsort.sorted_Nil,Qsort.sorted_Cons,
-  Qsort.qsort_Nil,Qsort.qsort_Cons];
-
+val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons];
 
-goal Qsort.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
-
-goal Qsort.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
-\                   mset(xs, x)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
 
 goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
@@ -63,13 +49,11 @@
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-val prems = goal Qsort.thy
- "[| !x y. (~le(x,y)) = le(y,x); \
-\    !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \
-\ sorted(le,qsort(le,xs))";
+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(ALLGOALS(asm_full_simp_tac (ss addsimps [hd prems,list_all_mem_conv]) ));
-by(cut_facts_tac (tl prems) 1);
+by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) ));
+by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by(fast_tac HOL_cs 1);
 result();
 
@@ -77,10 +61,10 @@
 (* A verification based on predicate calculus rather than combinators *)
 
 val sorted_Cons =
-  rewrite_rule [list_all_mem_conv RS eq_reflection] Qsort.sorted_Cons;
+  rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons;
 
 val ss = list_ss addsimps
- [Qsort.sorted_Nil,sorted_Cons,
+ [Sorting.sorted_Nil,sorted_Cons,
   Qsort.qsort_Nil,Qsort.qsort_Cons];
 
 
@@ -98,14 +82,11 @@
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-val prems = goal Qsort.thy
- "[| !x y. (~le(x,y)) = le(y,x); \
-\    !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \
-\ sorted(le,qsort(le,xs))";
+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 ss 1);
-by(asm_full_simp_tac (ss addsimps [hd prems]
-                         setloop (split_tac [expand_if])) 1);
-by(cut_facts_tac (tl prems) 1);
+by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1);
+by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by(fast_tac HOL_cs 1);
 result();
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/Qsort.thy
--- a/ex/Qsort.thy	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/Qsort.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -6,20 +6,12 @@
 Quicksort
 *)
 
-Qsort = List +
+Qsort = Sorting +
 consts
-  sorted :: "[['a,'a] => bool, 'a list] => bool"
-  mset   :: "'a list => ('a => nat)"
   qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
 
 rules
 
-sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
-
-mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
-
 qsort_Nil  "qsort(le,[]) = []"
 qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
 \                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/ROOT.ML
--- a/ex/ROOT.ML	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/ROOT.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -10,16 +10,17 @@
 
 writeln"Root file for HOL examples";
 proof_timing := true;
+loadpath := ["ex"];
 time_use     "ex/cla.ML";
 time_use     "ex/meson.ML";
 time_use     "ex/mesontest.ML";
-time_use_thy "ex/Qsort";
-time_use_thy "ex/LexProd";
-time_use_thy "ex/Puzzle";
+time_use_thy "InSort";
+time_use_thy "Qsort";
+time_use_thy "LexProd";
+time_use_thy "Puzzle";
 time_use     "ex/set.ML";
-time_use_thy "ex/Finite";
-time_use_thy "ex/PL";
-time_use_thy "ex/Term";
-time_use_thy "ex/Simult";
-time_use_thy "ex/MT";
+time_use_thy "PL";
+time_use_thy "Term";
+time_use_thy "Simult";
+time_use_thy "MT";
 maketest     "END: Root file for HOL examples";
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/Sorting.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Sorting.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,26 @@
+(*  Title: 	HOL/ex/sorting.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Some general lemmas
+*)
+
+val sorting_ss = list_ss 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_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
+val mset_app_distr = result();
+
+goal Sorting.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
+\                     mset(xs, x)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
+val mset_compl_add = result();
+
+val sorting_ss = sorting_ss addsimps
+      [mset_app_distr, mset_compl_add];
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/Sorting.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Sorting.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,31 @@
+(*  Title: 	HOL/ex/sorting.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Specifikation of sorting
+*)
+
+Sorting = List +
+consts
+  sorted1:: "[['a,'a] => bool, 'a list] => bool"
+  sorted :: "[['a,'a] => bool, 'a list] => bool"
+  mset   :: "'a list => ('a => nat)"
+  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,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+
+sorted_Nil "sorted(le,[])"
+sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+
+mset_Nil "mset([],y) = 0"
+mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+
+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
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/insort.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/insort.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,46 @@
+(*  Title: 	HOL/ex/insort.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Correctness proof of insertion sort.
+*)
+
+val insort_ss = sorting_ss addsimps
+ [InSort.ins_Nil,InSort.ins_Cons,InSort.insort_Nil,InSort.insort_Cons];
+
+goalw InSort.thy [Sorting.total_def]
+  "!!f. [| total(f); ~f(x,y) |] ==> f(y,x)";
+by(fast_tac HOL_cs 1);
+val totalD = result();
+
+goalw InSort.thy [Sorting.transf_def]
+  "!!f. [| transf(f); f(b,a) |] ==> !x. f(a,x) --> f(b,x)";
+by(fast_tac HOL_cs 1);
+val transfD = result();
+
+goal InSort.thy "list_all(p,ins(f,x,xs)) = (list_all(p,xs) & p(x))";
+by(list_ind_tac "xs" 1);
+by(asm_simp_tac insort_ss 1);
+by(asm_simp_tac (insort_ss setloop (split_tac [expand_if])) 1);
+by(fast_tac HOL_cs 1);
+val insort_ss = insort_ss addsimps [result()];
+
+goal InSort.thy "(!x. p(x) --> q(x)) --> list_all(p,xs) --> list_all(q,xs)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
+val list_all_imp = result();
+
+val prems = goal InSort.thy
+  "[| total(f); transf(f) |] ==>  sorted(f,ins(f,x,xs)) = sorted(f,xs)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
+by(cut_facts_tac prems 1);
+by(cut_inst_tac [("p","f(xa)"),("q","f(x)")] list_all_imp 1);
+by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
+val insort_ss = insort_ss addsimps [result()];
+
+goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted(f,insort(f,xs))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac insort_ss));
+result();
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/insort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/insort.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,22 @@
+(*  Title: 	HOL/ex/insort.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Insertion sort
+*)
+
+InSort  =  Sorting +
+
+consts
+  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
+  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
+
+rules
+  ins_Nil  "ins(f,x,[]) = [x]"
+  ins_Cons "ins(f,x,Cons(y,ys)) =   \
+\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+
+  insort_Nil  "insort(f,[]) = []"
+  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+end
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/qsort.ML
--- a/ex/qsort.ML	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/qsort.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -6,22 +6,8 @@
 Two verifications of Quicksort
 *)
 
-val ss = list_ss addsimps
- [Qsort.mset_Nil,Qsort.mset_Cons,
-  Qsort.sorted_Nil,Qsort.sorted_Cons,
-  Qsort.qsort_Nil,Qsort.qsort_Cons];
-
+val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons];
 
-goal Qsort.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
-
-goal Qsort.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
-\                   mset(xs, x)";
-by(list_ind_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
-val ss = ss addsimps [result()];
 
 goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
@@ -63,13 +49,11 @@
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-val prems = goal Qsort.thy
- "[| !x y. (~le(x,y)) = le(y,x); \
-\    !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \
-\ sorted(le,qsort(le,xs))";
+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(ALLGOALS(asm_full_simp_tac (ss addsimps [hd prems,list_all_mem_conv]) ));
-by(cut_facts_tac (tl prems) 1);
+by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) ));
+by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by(fast_tac HOL_cs 1);
 result();
 
@@ -77,10 +61,10 @@
 (* A verification based on predicate calculus rather than combinators *)
 
 val sorted_Cons =
-  rewrite_rule [list_all_mem_conv RS eq_reflection] Qsort.sorted_Cons;
+  rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons;
 
 val ss = list_ss addsimps
- [Qsort.sorted_Nil,sorted_Cons,
+ [Sorting.sorted_Nil,sorted_Cons,
   Qsort.qsort_Nil,Qsort.qsort_Cons];
 
 
@@ -98,14 +82,11 @@
 by(fast_tac HOL_cs 1);
 val ss = ss addsimps [result()];
 
-val prems = goal Qsort.thy
- "[| !x y. (~le(x,y)) = le(y,x); \
-\    !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \
-\ sorted(le,qsort(le,xs))";
+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 ss 1);
-by(asm_full_simp_tac (ss addsimps [hd prems]
-                         setloop (split_tac [expand_if])) 1);
-by(cut_facts_tac (tl prems) 1);
+by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1);
+by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
 by(fast_tac HOL_cs 1);
 result();
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/qsort.thy
--- a/ex/qsort.thy	Wed Feb 16 15:13:53 1994 +0100
+++ b/ex/qsort.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -6,20 +6,12 @@
 Quicksort
 *)
 
-Qsort = List +
+Qsort = Sorting +
 consts
-  sorted :: "[['a,'a] => bool, 'a list] => bool"
-  mset   :: "'a list => ('a => nat)"
   qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
 
 rules
 
-sorted_Nil "sorted(le,[])"
-sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
-
-mset_Nil "mset([],y) = 0"
-mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
-
 qsort_Nil  "qsort(le,[]) = []"
 qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
 \                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/sorting.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/sorting.ML	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,26 @@
+(*  Title: 	HOL/ex/sorting.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Some general lemmas
+*)
+
+val sorting_ss = list_ss 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_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
+val mset_app_distr = result();
+
+goal Sorting.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \
+\                     mset(xs, x)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if]))));
+val mset_compl_add = result();
+
+val sorting_ss = sorting_ss addsimps
+      [mset_app_distr, mset_compl_add];
diff -r 3d5b2b874e14 -r a73f8a7784bd ex/sorting.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/sorting.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,31 @@
+(*  Title: 	HOL/ex/sorting.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Specifikation of sorting
+*)
+
+Sorting = List +
+consts
+  sorted1:: "[['a,'a] => bool, 'a list] => bool"
+  sorted :: "[['a,'a] => bool, 'a list] => bool"
+  mset   :: "'a list => ('a => nat)"
+  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,Cons(y,zs))) = (f(x,y) & sorted1(f,Cons(y,zs)))"
+
+sorted_Nil "sorted(le,[])"
+sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
+
+mset_Nil "mset([],y) = 0"
+mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
+
+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