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();