equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/AllocBase |
1 (* Title: HOL/UNITY/AllocBase.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Basis declarations for Chandy and Charpentier's Allocator |
6 Basis declarations for Chandy and Charpentier's Allocator |
7 |
|
8 add_path "../Induct"; |
|
9 time_use_thy "AllocBase"; |
|
10 *) |
7 *) |
11 |
8 |
12 Goal "!!f :: nat=>nat. \ |
9 Goal "!!f :: nat=>nat. \ |
13 \ (ALL i. i<n --> f i <= g i) --> \ |
10 \ (ALL i. i<n --> f i <= g i) --> \ |
14 \ setsum f (lessThan n) <= setsum g (lessThan n)"; |
11 \ setsum f (lessThan n) <= setsum g (lessThan n)"; |
40 Goal "mono (bag_of :: 'a list => ('a::order) multiset)"; |
37 Goal "mono (bag_of :: 'a list => ('a::order) multiset)"; |
41 by (rtac monoI 1); |
38 by (rtac monoI 1); |
42 by (rewtac prefix_def); |
39 by (rewtac prefix_def); |
43 by (etac genPrefix.induct 1); |
40 by (etac genPrefix.induct 1); |
44 by Auto_tac; |
41 by Auto_tac; |
45 by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); |
42 by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1); |
46 by (etac order_trans 1); |
43 by (etac order_trans 1); |
47 by (rtac union_upper1 1); |
44 by (rtac (thm "union_upper1") 1); |
48 qed "mono_bag_of"; |
45 qed "mono_bag_of"; |
49 |
46 |
50 (** setsum **) |
47 (** setsum **) |
51 |
48 |
52 Addcongs [setsum_cong]; |
49 Addcongs [setsum_cong]; |