ex/Qsort.ML
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 46 a73f8a7784bd
child 55 d9096849bd8e
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     1
(*  Title: 	HOL/ex/qsort.ML
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     2
    ID:         $Id$
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     3
    Author: 	Tobias Nipkow
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     4
    Copyright   1994 TU Muenchen
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     5
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     6
Two verifications of Quicksort
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     7
*)
65a546c2b8ed changed header
nipkow
parents: 36
diff changeset
     8
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
     9
val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons];
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    10
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    11
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    12
goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    13
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    14
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    15
result();
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    16
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    17
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    18
goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    19
by(list_ind_tac "xs" 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    20
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    21
val ss = ss addsimps [result()];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    22
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    23
goal Qsort.thy
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    24
 "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    25
by(list_ind_tac "xs" 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    26
by(ALLGOALS(asm_simp_tac ss));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    27
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    28
val ss = ss addsimps [result()];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    29
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    30
goal Qsort.thy "(list_all(p,xs) & Q & list_all(q,ys)) = \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    31
\               (Q & list_all(p,xs) & list_all(q,ys))";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    32
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    33
val lemma1 = result();
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    34
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    35
goal HOL.thy "((~P --> Q) & (P --> Q)) = Q";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    36
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    37
val lemma2 = result();
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    38
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    39
goal Qsort.thy "(Alls x:qsort(le,xs).P(x))  =  (Alls x:xs.P(x))";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    40
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    41
by(ALLGOALS(asm_simp_tac (ss addsimps [lemma1,lemma2])));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    42
val ss = ss addsimps [result()];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    43
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    44
goal Qsort.thy
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    45
 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    46
\                     (Alls x:xs. Alls y:ys. le(x,y)))";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    47
by(list_ind_tac "xs" 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    48
by(ALLGOALS(asm_simp_tac ss));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    49
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    50
val ss = ss addsimps [result()];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    51
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    52
goal Qsort.thy 
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    53
 "!!le. [| total(le); transf(le) |] ==>  sorted(le,qsort(le,xs))";
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    54
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    55
by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) ));
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    56
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    57
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    58
result();
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    59
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    60
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    61
(* A verification based on predicate calculus rather than combinators *)
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    62
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    63
val sorted_Cons =
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    64
  rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons;
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    65
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    66
val ss = list_ss addsimps
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    67
 [Sorting.sorted_Nil,sorted_Cons,
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    68
  Qsort.qsort_Nil,Qsort.qsort_Cons];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    69
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    70
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    71
goal Qsort.thy "x mem qsort(le,xs)  =  x mem xs";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    72
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    73
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    74
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    75
val ss = ss addsimps [result()];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    76
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    77
goal Qsort.thy
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    78
 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    79
\                     (!x. x mem xs --> (!y. y mem ys --> le(x,y))))";
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    80
by(list_ind_tac "xs" 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    81
by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if]))));
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    82
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    83
val ss = ss addsimps [result()];
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    84
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    85
goal Qsort.thy
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    86
  "!!xs. [| total(le); transf(le) |] ==>  sorted(le,qsort(le,xs))";
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    87
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    88
by(simp_tac ss 1);
46
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    89
by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1);
a73f8a7784bd some more sorting algorithms
nipkow
parents: 44
diff changeset
    90
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    91
by(fast_tac HOL_cs 1);
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    92
result();