src/HOL/UNITY/AllocBase.ML
author paulson
Fri Jun 23 10:33:11 2000 +0200 (2000-06-23)
changeset 9109 0085c32a533b
parent 9107 67202a50ee6d
child 9336 9ae89b9ce206
permissions -rw-r--r--
sum_below f n -> setsum f (lessThan n)
     1 (*  Title:      HOL/UNITY/AllocBase
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Basis declarations for Chandy and Charpentier's Allocator
     7 
     8 add_path "../Induct";
     9 time_use_thy "AllocBase";
    10 *)
    11 
    12 Goal "!!f :: nat=>nat. \
    13 \     (ALL i. i<n --> f i <= g i) --> \
    14 \     setsum f (lessThan n) <= setsum g (lessThan n)";
    15 by (induct_tac "n" 1);
    16 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
    17 by (dres_inst_tac [("x","n")] spec 1);
    18 by (arith_tac 1);
    19 qed_spec_mp "setsum_fun_mono";
    20 
    21 Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    22 by (induct_tac "ys" 1);
    23 by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
    24 qed_spec_mp "tokens_mono_prefix";
    25 
    26 Goalw [mono_def] "mono tokens";
    27 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    28 qed "mono_tokens";
    29 
    30 
    31 (*** sublist ***)
    32 
    33 Goalw [sublist_def] "sublist l {} = []";
    34 by Auto_tac;
    35 qed "sublist_empty";
    36 
    37 Goalw [sublist_def] "sublist [] A = []";
    38 by Auto_tac;
    39 qed "sublist_nil";
    40 
    41 Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
    42 \     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
    43 by (res_inst_tac [("xs","xs")] rev_induct 1);
    44  by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
    45 by (Simp_tac 1);
    46 qed "sublist_shift_lemma";
    47 
    48 Goalw [sublist_def]
    49      "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
    50 by (res_inst_tac [("xs","l'")] rev_induct 1);
    51 by (Simp_tac 1);
    52 by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
    53 	                              zip_append, sublist_shift_lemma]) 1);
    54 by (asm_simp_tac (simpset() addsimps [add_commute]) 1);
    55 qed "sublist_append";
    56 
    57 Addsimps [sublist_empty, sublist_nil];
    58 
    59 Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
    60 by (res_inst_tac [("xs","l")] rev_induct 1);
    61  by (asm_simp_tac (simpset() delsimps [append_Cons]
    62 	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
    63 by (simp_tac (simpset() addsimps [sublist_def]) 1);
    64 qed "sublist_Cons";
    65 
    66 Goal "sublist [x] A = (if 0 : A then [x] else [])";
    67 by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
    68 qed "sublist_singleton";
    69 Addsimps [sublist_singleton];
    70 
    71 Goal "sublist l {..n(} = take n l";
    72 by (res_inst_tac [("xs","l")] rev_induct 1);
    73  by (asm_simp_tac (simpset() addsplits [nat_diff_split]
    74                              addsimps [sublist_append]) 2);
    75 by (Simp_tac 1);
    76 qed "sublist_upt_eq_take";
    77 Addsimps [sublist_upt_eq_take];
    78 
    79 
    80 (** bag_of **)
    81 
    82 Goal "bag_of (l@l') = bag_of l + bag_of l'";
    83 by (induct_tac "l" 1);
    84  by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
    85 by (Simp_tac 1);
    86 qed "bag_of_append";
    87 Addsimps [bag_of_append];
    88 
    89 Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
    90 by (rtac monoI 1); 
    91 by (rewtac prefix_def);
    92 by (etac genPrefix.induct 1);
    93 by Auto_tac;
    94 by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
    95 by (etac order_trans 1); 
    96 by (rtac union_upper1 1); 
    97 qed "mono_bag_of";
    98 
    99 (** setsum **)
   100 
   101 Addcongs [setsum_cong];
   102 
   103 Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
   104 \     setsum (%i. {#f i#}) (A Int lessThan k)";
   105 by (rtac setsum_cong 1);
   106 by Auto_tac;  
   107 qed "bag_of_sublist_lemma";
   108 
   109 Goal "bag_of (sublist l A) = \
   110 \     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
   111 by (res_inst_tac [("xs","l")] rev_induct 1);
   112 by (Simp_tac 1);
   113 by (asm_simp_tac
   114     (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
   115                     nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
   116 qed "bag_of_sublist";
   117 
   118 
   119 Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
   120 \     bag_of (sublist l A) + bag_of (sublist l B)";
   121 by (subgoal_tac "A Int B Int {..length l(} = \
   122 \                (A Int {..length l(}) Int (B Int {..length l(})" 1);
   123 by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2, 
   124                                       setsum_Un_Int]) 1);
   125 by (Blast_tac 1);
   126 qed "bag_of_sublist_Un_Int";
   127 
   128 Goal "A Int B = {} \
   129 \     ==> bag_of (sublist l (A Un B)) = \
   130 \         bag_of (sublist l A) + bag_of (sublist l B)"; 
   131 by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
   132 qed "bag_of_sublist_Un_disjoint";
   133 
   134 Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
   135 \     ==> bag_of (sublist l (UNION I A)) =  \
   136 \         setsum (%i. bag_of (sublist l (A i))) I";  
   137 by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
   138 			    addsimps [bag_of_sublist]) 1);
   139 by (stac setsum_UN_disjoint 1);
   140 by Auto_tac;  
   141 qed_spec_mp "bag_of_sublist_UN_disjoint";