equal
deleted
inserted
replaced
11 |
11 |
12 Addsimps qsort.rules; |
12 Addsimps qsort.rules; |
13 |
13 |
14 goal thy "(x mem qsort (ord,l)) = (x mem l)"; |
14 goal thy "(x mem qsort (ord,l)) = (x mem l)"; |
15 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); |
15 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); |
16 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]))); |
16 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
17 by (Blast_tac 1); |
17 by (Blast_tac 1); |
18 qed "qsort_mem_stable"; |
18 qed "qsort_mem_stable"; |
19 |
19 |
20 |
20 |
21 (** The silly g function: example of nested recursion **) |
21 (** The silly g function: example of nested recursion **) |
28 by (trans_tac 1); |
28 by (trans_tac 1); |
29 qed "g_terminates"; |
29 qed "g_terminates"; |
30 |
30 |
31 goal thy "g x = 0"; |
31 goal thy "g x = 0"; |
32 by (res_inst_tac [("u","x")] g.induct 1); |
32 by (res_inst_tac [("u","x")] g.induct 1); |
33 by (ALLGOALS (asm_simp_tac (!simpset addsimps [g_terminates]))); |
33 by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates]))); |
34 qed "g_zero"; |
34 qed "g_zero"; |
35 |
35 |
36 (*** the contrived `mapf' ***) |
36 (*** the contrived `mapf' ***) |
37 |
37 |
38 (* proving the termination condition: *) |
38 (* proving the termination condition: *) |