author  wenzelm 
Fri, 10 Oct 1997 19:02:28 +0200  
changeset 3842  b55686a7b22c 
parent 3647  a64c8fbcd98f 
child 3919  c036caebfc75 
permissions  rwrr 
1465  1 
(* Title: HOL/ex/sorting.ML 
969  2 
ID: $Id$ 
1465  3 
Author: Tobias Nipkow 
969  4 
Copyright 1994 TU Muenchen 
5 

6 
Some general lemmas 

7 
*) 

8 

3842  9 
goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x"; 
2031  10 
by (list.induct_tac "xs" 1); 
11 
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); 

2517  12 
qed "mset_append"; 
969  13 

3842  14 
goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \ 
969  15 
\ mset xs x"; 
2031  16 
by (list.induct_tac "xs" 1); 
17 
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); 

969  18 
qed "mset_compl_add"; 
19 

2517  20 
Addsimps [mset_append, mset_compl_add]; 
21 

3842  22 
goal Sorting.thy "set xs = {x. mset xs x ~= 0}"; 
2517  23 
by (list.induct_tac "xs" 1); 
24 
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); 

25 
by (Fast_tac 1); 

3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset

26 
qed "set_via_mset"; 
2517  27 

28 
(* Equivalence of two definitions of `sorted' *) 

29 

30 
val prems = goalw Sorting.thy [transf_def] 

31 
"transf(le) ==> sorted1 le xs = sorted le xs"; 

32 
by (list.induct_tac "xs" 1); 

33 
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_list_case])))); 

34 
by (cut_facts_tac prems 1); 

35 
by (Fast_tac 1); 

36 
qed "sorted1_is_sorted"; 