equal
deleted
inserted
replaced
1 (* Title: CCL/ex/list |
1 (* Title: CCL/ex/list |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 For list.thy. |
6 For list.thy. |
7 *) |
7 *) |
8 |
8 |
30 val list_ss = nat_ss addsimps listBs; |
30 val list_ss = nat_ss addsimps listBs; |
31 |
31 |
32 (****) |
32 (****) |
33 |
33 |
34 val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []"; |
34 val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []"; |
35 br (prem RS Nat_ind) 1; |
35 by (rtac (prem RS Nat_ind) 1); |
36 by (ALLGOALS (asm_simp_tac list_ss)); |
36 by (ALLGOALS (asm_simp_tac list_ss)); |
37 qed "nmapBnil"; |
37 qed "nmapBnil"; |
38 |
38 |
39 val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"; |
39 val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"; |
40 br (prem RS Nat_ind) 1; |
40 by (rtac (prem RS Nat_ind) 1); |
41 by (ALLGOALS (asm_simp_tac list_ss)); |
41 by (ALLGOALS (asm_simp_tac list_ss)); |
42 qed "nmapBcons"; |
42 qed "nmapBcons"; |
43 |
43 |
44 (***) |
44 (***) |
45 |
45 |
83 |
83 |
84 val prems = goalw List.thy [partition_def] |
84 val prems = goalw List.thy [partition_def] |
85 "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)"; |
85 "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)"; |
86 by (typechk_tac prems 1); |
86 by (typechk_tac prems 1); |
87 by clean_ccs_tac; |
87 by clean_ccs_tac; |
88 br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2; |
88 by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2); |
89 br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1; |
89 by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1); |
90 by (REPEAT (atac 1)); |
90 by (REPEAT (atac 1)); |
91 qed "partitionT"; |
91 qed "partitionT"; |
92 |
92 |
93 (*** Correctness Conditions for Insertion Sort ***) |
93 (*** Correctness Conditions for Insertion Sort ***) |
94 |
94 |