Turned into Isar theories.
authornipkow
Fri May 17 15:40:59 2002 +0200 (2002-05-17)
changeset 131592af7b94892ce
parent 13158 8e86582a90d1
child 13160 eca781285662
Turned into Isar theories.
src/HOL/IsaMakefile
src/HOL/ex/InSort.ML
src/HOL/ex/InSort.thy
src/HOL/ex/Qsort.ML
src/HOL/ex/Qsort.thy
src/HOL/ex/Sorting.ML
src/HOL/ex/Sorting.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri May 17 11:36:32 2002 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 17 15:40:59 2002 +0200
     1.3 @@ -569,12 +569,12 @@
     1.4  
     1.5  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
     1.6    ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
     1.7 -  ex/Hilbert_Classical.thy ex/InSort.ML ex/InSort.thy ex/IntRing.ML \
     1.8 +  ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
     1.9    ex/IntRing.thy ex/Intuitionistic.thy \
    1.10    ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy \
    1.11    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
    1.12    ex/NatSum.thy ex/PER.thy ex/Primrec.thy ex/Puzzle.thy \
    1.13 -  ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
    1.14 +  ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
    1.15    ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.16    ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
    1.17    ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
     2.1 --- a/src/HOL/ex/InSort.ML	Fri May 17 11:36:32 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,37 +0,0 @@
     2.4 -(*  Title:      HOL/ex/insort.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   1994 TU Muenchen
     2.8 -
     2.9 -Correctness proof of insertion sort.
    2.10 -*)
    2.11 -
    2.12 -Goal "!y. multiset(ins le x xs) y = multiset (x#xs) y";
    2.13 -by (induct_tac "xs" 1);
    2.14 -by Auto_tac;
    2.15 -qed_spec_mp "multiset_ins";
    2.16 -Addsimps [multiset_ins];
    2.17 -
    2.18 -Goal "!x. multiset(insort le xs) x = multiset xs x";
    2.19 -by (induct_tac "xs" 1);
    2.20 -by Auto_tac;
    2.21 -qed_spec_mp "insort_permutes";
    2.22 -
    2.23 -Goal "set(ins le x xs) = insert x (set xs)";
    2.24 -by (asm_simp_tac (simpset() addsimps [set_via_multiset]) 1);
    2.25 -by (Fast_tac 1);
    2.26 -qed "set_ins";
    2.27 -Addsimps [set_ins];
    2.28 -
    2.29 -Goal "total(le) --> transf(le) --> sorted le (ins le x xs) = sorted le xs";
    2.30 -by (induct_tac "xs" 1);
    2.31 -by (ALLGOALS Asm_simp_tac);
    2.32 -by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
    2.33 -by (Blast_tac 1);
    2.34 -qed_spec_mp "sorted_ins";
    2.35 -Addsimps [sorted_ins];
    2.36 -
    2.37 -Goal "[| total(le); transf(le) |] ==>  sorted le (insort le xs)";
    2.38 -by (induct_tac "xs" 1);
    2.39 -by Auto_tac;
    2.40 -qed "sorted_insort";
     3.1 --- a/src/HOL/ex/InSort.thy	Fri May 17 11:36:32 2002 +0200
     3.2 +++ b/src/HOL/ex/InSort.thy	Fri May 17 15:40:59 2002 +0200
     3.3 @@ -6,17 +6,43 @@
     3.4  Insertion sort
     3.5  *)
     3.6  
     3.7 -InSort  =  Sorting +
     3.8 +theory InSort  =  Sorting:
     3.9  
    3.10  consts
    3.11 -  ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
    3.12 -  insort :: [['a,'a]=>bool, 'a list] => 'a list
    3.13 +  ins :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.14 +  insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.15  
    3.16  primrec
    3.17    "ins le x [] = [x]"
    3.18    "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"
    3.19 +
    3.20  primrec
    3.21    "insort le [] = []"
    3.22    "insort le (x#xs) = ins le x (insort le xs)"
    3.23 +
    3.24 +
    3.25 +lemma multiset_ins[simp]:
    3.26 + "\<And>y. multiset(ins le x xs) y = multiset (x#xs) y"
    3.27 +by (induct "xs") auto
    3.28 +
    3.29 +lemma insort_permutes[simp]:
    3.30 + "\<And>x. multiset(insort le xs) x = multiset xs x";
    3.31 +by (induct "xs") auto
    3.32 +
    3.33 +lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)"
    3.34 +by (simp add: set_via_multiset) fast
    3.35 +
    3.36 +lemma sorted_ins[simp]:
    3.37 + "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
    3.38 +apply (induct xs)
    3.39 +apply simp_all
    3.40 +apply (unfold Sorting.total_def Sorting.transf_def)
    3.41 +apply blast
    3.42 +done
    3.43 +
    3.44 +lemma sorted_insort:
    3.45 + "[| total(le); transf(le) |] ==>  sorted le (insort le xs)"
    3.46 +by (induct xs) auto
    3.47 +
    3.48  end
    3.49  
     4.1 --- a/src/HOL/ex/Qsort.ML	Fri May 17 11:36:32 2002 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,49 +0,0 @@
     4.4 -(*  Title:      HOL/ex/Qsort.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow (tidied by lcp)
     4.7 -    Copyright   1994 TU Muenchen
     4.8 -
     4.9 -The verification of Quicksort
    4.10 -*)
    4.11 -
    4.12 -(*** Version one: higher-order ***)
    4.13 -
    4.14 -Goal "multiset (qsort(le,xs)) x = multiset xs x";
    4.15 -by (induct_thm_tac qsort.induct "le xs" 1);
    4.16 -by Auto_tac;
    4.17 -qed "qsort_permutes";
    4.18 -Addsimps [qsort_permutes];
    4.19 -
    4.20 -(*Also provable by induction*)
    4.21 -Goal "set (qsort(le,xs)) = set xs";
    4.22 -by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
    4.23 -qed "set_qsort";
    4.24 -Addsimps [set_qsort];
    4.25 -
    4.26 -Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
    4.27 -by (induct_thm_tac qsort.induct "le xs" 1);
    4.28 -by (ALLGOALS Asm_simp_tac);
    4.29 -by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
    4.30 -by (Blast_tac 1);
    4.31 -qed_spec_mp "sorted_qsort";
    4.32 -
    4.33 -
    4.34 -(*** Version two: type classes ***)
    4.35 -
    4.36 -Goal "multiset (quickSort xs) z = multiset xs z";
    4.37 -by (res_inst_tac [("x","xs")] quickSort.induct 1);
    4.38 -by Auto_tac;
    4.39 -qed "quickSort_permutes";
    4.40 -Addsimps [quickSort_permutes];
    4.41 -
    4.42 -(*Also provable by induction*)
    4.43 -Goal "set (quickSort xs) = set xs";
    4.44 -by (simp_tac (simpset() addsimps [set_via_multiset]) 1);
    4.45 -qed "set_quickSort";
    4.46 -Addsimps [set_quickSort];
    4.47 -
    4.48 -Goal "sorted (op <=) (quickSort xs)";
    4.49 -by (res_inst_tac [("x","xs")] quickSort.induct 1);
    4.50 -by (ALLGOALS Asm_simp_tac);
    4.51 -by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1);
    4.52 -qed_spec_mp "sorted_quickSort";
     5.1 --- a/src/HOL/ex/Qsort.thy	Fri May 17 11:36:32 2002 +0200
     5.2 +++ b/src/HOL/ex/Qsort.thy	Fri May 17 15:40:59 2002 +0200
     5.3 @@ -6,28 +6,58 @@
     5.4  Quicksort
     5.5  *)
     5.6  
     5.7 -Qsort = Sorting +
     5.8 +theory Qsort = Sorting:
     5.9  
    5.10  (*Version one: higher-order*)
    5.11 -consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
    5.12 +consts qsort :: "('a \<Rightarrow> 'a => bool) * 'a list \<Rightarrow> 'a list"
    5.13  
    5.14  recdef qsort "measure (size o snd)"
    5.15 -    simpset "simpset() addsimps [length_filter RS le_less_trans]"
    5.16 -    
    5.17 -    "qsort(le, [])   = []"
    5.18 -    
    5.19 -    "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
    5.20 -                       @ (x # qsort(le, [y:xs . le x y]))"
    5.21 +"qsort(le, [])   = []"
    5.22 +"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
    5.23 +                   qsort(le, [y:xs . le x y])"
    5.24 +(hints recdef_simp: length_filter[THEN le_less_trans])
    5.25 +
    5.26 +lemma qsort_permutes[simp]:
    5.27 + "multiset (qsort(le,xs)) x = multiset xs x"
    5.28 +by (induct le xs rule: qsort.induct, auto)
    5.29 +
    5.30 +
    5.31 +(*Also provable by induction*)
    5.32 +lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
    5.33 +by(simp add: set_via_multiset)
    5.34 +
    5.35 +lemma sorted_qsort:
    5.36 + "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
    5.37 +apply (induct le xs rule: qsort.induct)
    5.38 + apply simp
    5.39 +apply simp
    5.40 +apply(unfold Sorting.total_def Sorting.transf_def)
    5.41 +apply blast
    5.42 +done
    5.43  
    5.44  
    5.45  (*Version two: type classes*)
    5.46 +
    5.47  consts quickSort :: "('a::linorder) list => 'a list"
    5.48  
    5.49  recdef quickSort "measure size"
    5.50 -    simpset "simpset() addsimps [length_filter RS le_less_trans]"
    5.51 -    
    5.52 -    "quickSort []   = []"
    5.53 -    
    5.54 -    "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ (x # quickSort [y:l. x<=y])"
    5.55 +"quickSort []   = []"
    5.56 +"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
    5.57 +(hints recdef_simp: length_filter[THEN le_less_trans])
    5.58 +
    5.59 +lemma quickSort_permutes[simp]:
    5.60 + "multiset (quickSort xs) z = multiset xs z"
    5.61 +by (induct xs rule: quickSort.induct) auto
    5.62 +
    5.63 +(*Also provable by induction*)
    5.64 +lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
    5.65 +by(simp add: set_via_multiset)
    5.66 +
    5.67 +lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
    5.68 +apply (induct xs rule: quickSort.induct)
    5.69 + apply simp
    5.70 +apply simp
    5.71 +apply(blast intro: linorder_linear[THEN disjE] order_trans)
    5.72 +done
    5.73  
    5.74  end
     6.1 --- a/src/HOL/ex/Sorting.ML	Fri May 17 11:36:32 2002 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,41 +0,0 @@
     6.4 -(*  Title:      HOL/ex/sorting.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Tobias Nipkow
     6.7 -    Copyright   1994 TU Muenchen
     6.8 -
     6.9 -Some general lemmas
    6.10 -*)
    6.11 -
    6.12 -Goal "multiset (xs@ys) x = multiset xs x + multiset ys x";
    6.13 -by (induct_tac "xs" 1);
    6.14 -by Auto_tac;
    6.15 -qed "multiset_append";
    6.16 -
    6.17 -Goal "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
    6.18 -by (induct_tac "xs" 1);
    6.19 -by Auto_tac;
    6.20 -qed "multiset_compl_add";
    6.21 -
    6.22 -Addsimps [multiset_append, multiset_compl_add];
    6.23 -
    6.24 -Goal "set xs = {x. multiset xs x ~= 0}";
    6.25 -by (induct_tac "xs" 1);
    6.26 -by Auto_tac;
    6.27 -qed "set_via_multiset";
    6.28 -
    6.29 -(* Equivalence of two definitions of `sorted' *)
    6.30 -
    6.31 -Goal "transf(le) ==> sorted1 le xs = sorted le xs";
    6.32 -by (induct_tac "xs" 1);
    6.33 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [list.split])));
    6.34 -by (rewtac transf_def);
    6.35 -by (Blast_tac 1);
    6.36 -qed "sorted1_is_sorted";
    6.37 -
    6.38 -Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
    6.39 -\                         (ALL x:set xs. ALL y:set ys. le x y))";
    6.40 -by (induct_tac "xs" 1);
    6.41 -by Auto_tac;
    6.42 -qed "sorted_append";
    6.43 -Addsimps [sorted_append];
    6.44 -
     7.1 --- a/src/HOL/ex/Sorting.thy	Fri May 17 11:36:32 2002 +0200
     7.2 +++ b/src/HOL/ex/Sorting.thy	Fri May 17 15:40:59 2002 +0200
     7.3 @@ -6,11 +6,12 @@
     7.4  Specification of sorting
     7.5  *)
     7.6  
     7.7 -Sorting = Main +
     7.8 +theory Sorting = Main:
     7.9 +
    7.10  consts
    7.11 -  sorted1:: [['a,'a] => bool, 'a list] => bool
    7.12 -  sorted :: [['a,'a] => bool, 'a list] => bool
    7.13 -  multiset   :: 'a list => ('a => nat)
    7.14 +  sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    7.15 +  sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    7.16 +  multiset   :: "'a list => ('a => nat)"
    7.17  
    7.18  primrec
    7.19    "sorted1 le [] = True"
    7.20 @@ -26,10 +27,39 @@
    7.21    "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
    7.22  
    7.23  constdefs
    7.24 -  total  :: (['a,'a] => bool) => bool
    7.25 +  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    7.26     "total r == (ALL x y. r x y | r y x)"
    7.27    
    7.28 -  transf :: (['a,'a] => bool) => bool
    7.29 +  transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    7.30     "transf f == (ALL x y z. f x y & f y z --> f x z)"
    7.31  
    7.32 +(* Some general lemmas *)
    7.33 +
    7.34 +lemma multiset_append[simp]:
    7.35 + "multiset (xs@ys) x = multiset xs x + multiset ys x"
    7.36 +by (induct xs, auto)
    7.37 +
    7.38 +lemma multiset_compl_add[simp]:
    7.39 + "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
    7.40 +by (induct xs, auto)
    7.41 +
    7.42 +lemma set_via_multiset: "set xs = {x. multiset xs x ~= 0}";
    7.43 +by (induct xs, auto)
    7.44 +
    7.45 +(* Equivalence of two definitions of `sorted' *)
    7.46 +
    7.47 +lemma sorted1_is_sorted:
    7.48 + "transf(le) ==> sorted1 le xs = sorted le xs";
    7.49 +apply(induct xs)
    7.50 + apply simp
    7.51 +apply(simp split: list.split)
    7.52 +apply(unfold transf_def);
    7.53 +apply(blast)
    7.54 +done
    7.55 +
    7.56 +lemma sorted_append[simp]:
    7.57 + "sorted le (xs@ys) = (sorted le xs \<and> sorted le ys \<and>
    7.58 +                       (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
    7.59 +by (induct xs, auto)
    7.60 +
    7.61  end