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