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 


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 


14 
goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \


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 


22 
goal Sorting.thy "set_of_list xs = {x.mset xs x ~= 0}";


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


24 
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));


25 
by (Fast_tac 1);


26 
qed "set_of_list_via_mset";


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";
